proposition: Lemma Idl_Comma : Idl_law Comp_Comma Id_Comma.
proof: Proof. unfold Idl_law in |- *; intros a b f1; elim f1; intros h e. simpl in |- *; unfold Equal_com_arrow in |- *; simpl in |- *. unfold Comp_com_mor in |- *; simpl in |- *. apply Idl. Qed.
imports: Functor