proposition: Lemma JOIN_fmap_JOIN : JoinLaws.associativity (@JOIN').
proof: Proof. move=> A; rewrite {1 2}/JOIN' -[LHS]compA /=. rewrite -functor_o. rewrite Hprod4. rewrite {1}/JOIN. rewrite -(compA Join (M # prod) prod). rewrite functor_o. rewrite [LHS]compA. rewrite joinA. rewrite -compA. rewrite functor_o. rewrite (compA Join (M # (M # prod)) (M # prod)). by rewrite -(natural _). Qed.
imports: mathcomp(all_ssreflect) HB(structures) monae_lib hierarchy monad_lib