proposition: Lemma Comp_Functor_comp_law : Fcomp_law Comp_FMap.
proof: Proof. unfold Fcomp_law, Comp_FOb, Comp_FMap, Comp_FMor in |- *. simpl in |- *; intros a b c f g. apply Trans with (FMor H (FMor G f o FMor G g)). apply FPres; apply FComp. apply FComp. Qed.
imports: Setoid_dup1 Hom_Equality