proposition: Lemma ONE_ONE_def {A B : Type'} : (@ONE_ONE A B) = (fun _2064 : A -> B => forall x1 : A, forall x2 : A, ((_2064 x1) = (_2064 x2)) -> x1 = x2).
proof: Proof. exact (eq_refl (@ONE_ONE A B)). Qed.
imports: coq theory_hol types