proposition: Theorem ccc_apply : ∀ `{Repr a} `{Repr b} `{Repr c} (U : a → b → c) (U' : repr a ~{AST}~> repr c ^ repr b) (V : a → b) (V' : repr a ~{AST}~> repr b), U >===> U' -> V >==> V' -> (λ x, U x (V x)) >==> eval ∘ U' △ V'.
proof: Proof. unfold rel, rel2; repeat intros. rewrite <- comp_assoc. rewrite <- fork_comp. rewrites. rewrite <- eval_first. comp_left. unfold first. rewrite <- fork_comp. rewrite <- comp_assoc. rewrite <- convert_fork; cat. 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