proposition: Lemma joinA : JoinLaws.associativity join.
proof: Proof. move => A; rewrite funeqE => mmma. rewrite /join. rewrite bind_fmap_fun/= bindA/=. congr (fun f => bind f mmma). by rewrite hom_ext. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)