proposition: Lemma CONSTR_def {A : Type'} : (@CONSTR A) = (fun _17591 : nat => fun _17592 : A => fun _17593 : nat -> recspace A => @_mk_rec A (@ZCONSTR A _17591 _17592 (fun n : nat => @_dest_rec A (_17593 n)))).
proof: Proof. exact (eq_refl (@CONSTR A)). Qed.
imports: coq theory_hol types