proposition: Lemma Assoc_Comma : Assoc_law Comp_Comma.
proof: Proof. unfold Assoc_law in |- *; intros a b c d f1; elim f1. intros h1 e1 f2; elim f2; intros h2 e2 f3. elim f3; intros h3 e3. simpl in |- *; unfold Equal_com_arrow in |- *; simpl in |- *. unfold Comp_com_mor in |- *; simpl in |- *. unfold Comp_com_mor in |- *; simpl in |- *. apply Ass. Qed.
imports: Functor