fact: Definition mk_nadd : (nat -> nat) -> nadd := fun f => @ε (nadd') (mk_nadd_pred f).
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance ExtensionalityFacts List Coq.Strings.Ascii