fact: Definition _mk_rec : forall {A : Type'}, (nat -> A -> Prop) -> recspace A := fun A f => ε (_mk_rec_pred f).
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance