proposition: Lemma Comp_com_congl : Congl_law Comp_com_arrow.
proof: Proof. unfold Congl_law in |- *; simpl in |- *. intros a b c f1; elim f1; intros h e f2. elim f2; intros h' e' f3; elim f3; intros h'' e''. unfold Equal_com_arrow in |- *; simpl in |- *. unfold Comp_com_mor in |- *; simpl in |- *. intro H; apply Comp_l; trivial. Qed.
imports: Functor