proposition: Lemma axiom_9 : forall {A : Type'} (a : recspace A), (@_mk_rec A (@_dest_rec A a)) = a.
proof: Proof. intros A [f h]. simpl. apply eq_recspace. simpl. rewrite <- axiom_10. exact h. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance