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