proposition: Corollary exl_fork_comp {x y z w} (f : x ~> y) (g : x ~> z) (h : w ~> x) : exl ∘ ((f △ g) ∘ h) ≈ f ∘ h.
proof: Proof. rewrite comp_assoc. rewrite exl_fork. reflexivity. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Structure.Terminal