proposition: Lemma map_id : forall A (m : M A), id <$> m = m.
proof: Proof. intros ; rewrite /map /id /= /bind monad_law2 //. Qed.
imports: Coq(ssreflect ssrfun FunctionalExtensionality) Mon(SPropBase) Coq(Relation_Definitions Morphisms)