proposition: Lemma sfmap_as_bind_ret_applied `{Equiv A} `{Equiv B} `{!Setoid_Morphism (f : A → B)} (m : M A) : sfmap f m = x ← m ; ret (f x).
proof: Proof. pose proof (setoidmor_a f). now apply sfmap_as_bind_ret. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.functors