proposition: Lemma Comp_MonMor_congr : Congr_law Comp_MonMor.
proof: Proof. unfold Congr_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 Pres1. apply H. Qed.
imports: SET Monoid