proposition: Lemma project_embed_id : forall sm, embed (project sm) = sm.
proof: Proof. intro sm. apply sig_eq ; extensionality m0. cbv. move: (proj2_sig sm) => [m Hm]. pose (H0 := Hm m0). apply eq_sym in H0. unshelve eapply (eq_trans _ H0). f_equiv. pose (He := Hm (e M)). apply (eq_trans He). rewrite monoid_law2 //. Qed.
imports: Coq(ssreflect ssrfun ssrbool List) Coq(FunctionalExtensionality) Coq(Relation_Definitions Morphisms) Mon(SPropBase SPropMonadicStructures)