proposition: Lemma UNCURRY_def {A B C : Type'} : (@UNCURRY A B C) = (fun _1304 : A -> B -> C => fun _1305 : prod A B => _1304 (@fst A B _1305) (@snd A B _1305)).
proof: Proof. exact (eq_refl (@UNCURRY A B C)). Qed.
imports: coq theory_hol types