Description: This is the definition for the well-founded recursion generator.
Similar to df-wrecs and df-recs , it is a direct definition form of
normally recursive relationships. Unlike the former two definitions, it
only requires a well-founded set-like relationship for its properties,
not a well-ordered relationship. This proof requires either a partial
order or the axiom of infinity. We develop the theorems twice, once
with a partial order and once without. The second development occurs
later in the database, after ax-inf has been introduced. (Contributed by Scott Fenton, 23-Dec-2021)