proposition: Lemma join_sfmap_join_applied `{Setoid A} (m : M (M (M A))) : join (sfmap join m) = join (join m).
proof: Proof. now apply join_sfmap_join. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.functors