proposition: Theorem ccc_curry : ∀ `{Repr a} `{Repr b} `{Repr c} (U : a * b → c) (U' : repr a × repr b ~> repr c), U >==> U' -> (λ x, λ y, U (x, y)) >===> curry U'.
proof: Proof. unfold rel, rel2; repeat intros. rewrite uncurry_curry. apply X. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Structure.Terminal Category.Structure.Cartesian Category.Structure.Cartesian.Closed Category.Functor.Structure.Cartesian Category.Instance.Coq Category.Instance.AST Category.Tools.Represented