proposition: Lemma ZCONSTR_def {A : Type'} : (@ZCONSTR A) = (fun _17566 : nat => fun _17567 : A => fun _17568 : nat -> nat -> A -> Prop => @INJP A (@INJN A (S _17566)) (@INJP A (@INJA A _17567) (@INJF A _17568))).
proof: Proof. exact (eq_refl (@ZCONSTR A)). Qed.
imports: coq theory_hol types