proposition: Corollary fun_comp_assoc_sym {C D E B : Category} {F : E ⟶ B} {G : D ⟶ E} {H : C ⟶ D} : (F ◯ G) ◯ H ⟹ F ◯ (G ◯ H).
proof: Proof. transform; simpl; intros; cat. Defined.
imports: Category.Lib Category.Theory.Category Category.Theory.Functor