proposition: Lemma bind_join `{Setoid A} : bind join = join ∘ join.
proof: Proof. rewrite !join_as_bind. rewrite bind_assoc. now apply setoids.ext_equiv_refl. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.functors