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