proposition: Lemma bindA : BindLaws.associative (@bind M).
proof: Proof. move: (@bindA_derived M join joinA). rewrite (_ : bind_of_join _ = @bind M) //. apply funext_dep => A; apply funext_dep => B. apply funext_dep => m; apply funext_dep => f. by rewrite bindE. Qed.
imports: ssrmatching JMeq mathcomp(all_ssreflect) imonae_lib HB(structures)