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