proposition: Lemma comp_hom_assoc : forall (a b c d : C) (f : Hom a b) (g : Hom b c) (h : Hom c d), Equal (comp_hom (comp_hom h g) f) (comp_hom h (comp_hom g f)).
proof: Proof. exact (Hom_comp_assoc_prf (c:=C)). Qed.
imports: Cartesian