proposition: Lemma sfmap_join_applied `{Equiv A} `{Equiv B} `{!Setoid_Morphism (f : A → B)} (m : M (M A)) : sfmap f (join m) = join (sfmap (sfmap f) m).
proof: Proof. now apply sfmap_join. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.functors