proposition: Lemma CONSTR_INJ : forall {A : Type'}, forall c1 : nat, forall i1 : A, forall r1 : nat -> recspace A, forall c2 : nat, forall i2 : A, forall r2 : nat -> recspace A, ((@CONSTR A c1 i1 r1) = (@CONSTR A c2 i2 r2)) = ((c1 = c2) /\ ((i1 = i2) /\ (r1 = r2))).
proof: Proof. intros A c1 i1 r1 c2 i2 r2. apply prop_ext. 2: intros [e1 [e2 e3]]; subst; reflexivity. unfold CONSTR. intro e. apply MK_REC_INJ in e. apply ZCONSTR_INJ in e. destruct e as [e1 [e2 e3]]. split. auto. split. auto. apply fun_ext; intro x. apply eq_recspace. generalize (ext_fun e3 x). auto. split; apply ZRECSPACE1; intro n. destruct (r1 n). auto. destruct (r2 n). auto. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance