proposition: Lemma axiom_10 : forall {A : Type'} (r : nat -> A -> Prop), (@ZRECSPACE A r) = ((@_dest_rec A (@_mk_rec A r)) = r).
proof: Proof. intros A f. apply prop_ext. intro h. apply (@ε_spec _ (_mk_rec_pred f)). exists (exist _ _ h). reflexivity. intro e. rewrite <- e. destruct (_mk_rec f) as [g h]. simpl. exact h. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance