proposition: Lemma join_spec_applied_alt `{Setoid A} (m : M (M A)) : join m = x ← m ; x.
proof: Proof. now apply join_as_bind. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.functors