proposition: Lemma Assoc_CAT : Assoc_law' Comp_CAT.
proof: Proof. unfold Assoc_law', Cat_comp' in |- *; simpl in |- *. intros C D E F G H X. unfold Equal_Functor in |- *; simpl in |- *. unfold Ap2 in |- *; simpl in |- *; auto. Qed.
imports: IdCAT Category_dup1