proposition: Lemma bindA_derived : BindLaws.associative (bind_of_join join).
proof: Proof. move=> A B C m f g; rewrite /bind_of_join. rewrite [LHS](_ : _ = ((@join _ \o (F # g \o @join _) \o F # f) m)) //. rewrite (natural join) (compA (@join C)) -joinA -(compE (@join _)). transitivity ((@join _ \o F # (@join _ \o (F # g \o f))) m) => //. by rewrite -2!compA functor_o FCompE -[in LHS](@functor_o F). Qed.
imports: ssrmatching JMeq mathcomp(all_ssreflect) imonae_lib HB(structures)