proposition: Lemma Comp_MonMor_congl : Congl_law Comp_MonMor.
proof: Proof. unfold Congl_law in |- *; simpl in |- *. unfold Equal_MonMor, Ext in |- *; simpl in |- *. unfold Comp_fun in |- *. intros m1 m2 m3 f g h H a. apply H. Qed.
imports: SET Monoid