proposition: Lemma bind_join_applied `{Setoid A} (m : M (M (M A))) : m ≫= join = join (join m).
proof: Proof. now apply bind_join. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.functors