proposition: Lemma sfmap_ret_applied `{Equiv A} `{Equiv B} `{!Setoid_Morphism (f : A → B)} (x : A) : sfmap f (ret x) = ret (f x).
proof: Proof. now apply sfmap_ret. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.functors