proposition: Lemma Idl_MON : Idl_law Comp_MON Id_MON.
proof: Proof. unfold Idl_law in |- *; intros m1 m2 f; simpl in |- *. unfold Equal_MonMor, Ext in |- *; simpl in |- *. unfold Comp_fun in |- *; intro a. unfold Id_MON_map in |- *; simpl in |- *; unfold Id_fun in |- *. apply Refl. Qed.
imports: SET Monoid