proposition: Lemma map_ret {A B} (f : A -> B) (a : A) : f <$> ret a = @ret M _ (f a).
proof: Proof. rewrite /map /bind monad_law1 //. Qed.
imports: Coq(ssreflect ssrfun ssrbool) Coq(Relation_Definitions Morphisms) Mon(SPropBase SPropMonadicStructures MonadExamples SpecificationMonads DijkstraMonadExamples) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples)