proposition: Theorem ccc_apply_pair : ∀ `{Repr a} `{Repr b} `{Repr c} (U : a * b → c) (U' : repr a × repr b ~{AST}~> repr c) (V : a → b) (V' : repr a ~{AST}~> repr b), U >==> U' -> V >==> V' -> (λ x, U (x, V x)) >==> U' ∘ id △ V'.
proof: Proof. unfold rel; intros ??????? U' V; subst; intros. rewrite <- comp_assoc. rewrite <- fork_comp. rewrite id_left. rewrites. rewrite convert_fork. reflexivity. 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