proposition: Lemma law3 : BindLaws.associative (bind eps).
proof: Proof. rewrite /BindLaws.associative => A B C x ab bc. rewrite /bind. set N := M f g. set j := mu eps. rewrite [X in _ = j C X](_ : _ = (N # (j C)) ((N # (N # bc)) ((N # ab) x))); last first. rewrite functor_o. rewrite compE. congr ((N # j C) _). rewrite functor_o. by rewrite (compE _ _ x). move: muMA (muM_natural bc). rewrite -/N -/j. move=> muMA. have -> : (N # bc) (j B ((N # ab) x)) = (N # bc \o j B) ((N # ab) x) by []. move=> ->. rewrite compE. rewrite [LHS](_ : _ = (j C \o j (N C)) ((N # (N # bc)) ((N # ab) x))) //. by rewrite muMA. Qed.
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy