proposition: Lemma join_sfmap_ret_applied `{Setoid A} (m : M A): join (sfmap ret m) = m.
proof: Proof. now apply join_sfmap_ret. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.functors