proposition: Lemma Comp_Functor_congl : Congl_law' Comp_Functor.
proof: Proof. unfold Congl_law' in |- *; simpl in |- *. unfold Equal_Functor, Comp_Functor in |- *. intros A B C F G H eq_FG a1 a2 f. unfold FMor in |- *; simpl in |- *. unfold Comp_FOb, Comp_FMor in |- *. apply eq_FG. Qed.
imports: IdCAT Category_dup1