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