proposition: Lemma fun_strict_equiv_comp_assoc {A B C D} (F : C ⟶ D) (G : B ⟶ C) (H : A ⟶ B) : F ◯ (G ◯ H) ≈ (F ◯ G) ◯ H.
proof: Proof. construct; cat. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Equations.Prop.Logic