fact: Definition CONSTR {A : Type'} := 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))).
imports: coq theory_hol types