proposition: Lemma bind_as_join_sfmap_applied `{Equiv A} `{Setoid B} `{!Setoid_Morphism (f : A → M B)} (m : M A) : m ≫= f = join (sfmap f m).
proof: Proof. pose proof (setoidmor_a f). now apply bind_as_join_sfmap. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.functors