proposition: Lemma eq_recspace {A : Type'} : forall (f g : recspace A), _dest_rec f = _dest_rec g -> f = g.
proof: Proof. intros [f hf] [g hg]. simpl. intro e. subst g. apply subset_eq_compat. reflexivity. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance