proposition: Lemma Comp_MonMor_unit_law : MonUnit_law Comp_MonMor_map.
proof: Proof. unfold MonUnit_law, Comp_MonMor_map in |- *. simpl in |- *; unfold Comp_fun in |- *. apply Trans with (g (Munit m2)). apply Pres1; apply MMon_unit. apply MMon_unit. Qed.
imports: SET Monoid