proposition: Lemma axiom_20 : forall (r : nat -> nat), (is_nadd r) = ((dest_nadd (mk_nadd r)) = r).
proof: Proof. intro f. apply prop_ext. intro h. apply (@ε_spec (nadd') (mk_nadd_pred f)). exists (exist _ _ h). reflexivity. intro e. rewrite <- e. destruct (mk_nadd f) as [g h]. simpl. exact h. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance ExtensionalityFacts List Coq.Strings.Ascii