proposition: Lemma CURRY_def {A B C : Type'} : (@CURRY A B C) = (fun _1283 : (prod A B) -> C => fun _1284 : A => fun _1285 : B => _1283 (@pair A B _1284 _1285)).
proof: Proof. exact (eq_refl (@CURRY A B C)). Qed.
imports: coq theory_hol types