proposition: Lemma JOIN_fmap_JOIN : JoinLaws.associativity (@JOIN').
proof: Proof. move=> A. rewrite [JOIN' _]/=. rewrite [X in _ = _ \o X]/=. by rewrite !JOINE -!/prod (Prod.JOIN_fmap_JOIN prod1 prod4). Qed.
imports: mathcomp(all_ssreflect) HB(structures) monae_lib hierarchy monad_lib