proposition: Lemma Idl_CAT : Idl_law' Comp_CAT Id_CAT.
proof: Proof. unfold Idl_law', Cat_comp', Ap2 in |- *; simpl in |- *. intros C D G; unfold Comp_Functor, Equal_Functor in |- *. intros a b f; unfold FMor in |- *; simpl in |- *. unfold Comp_FMor in |- *; unfold Id_CAT, FMor in |- *; simpl in |- *. auto. Qed.
imports: IdCAT Category_dup1