proposition: Lemma associative : BindLaws.associative bindK.
proof: Proof. by move=> A B C m f g; rewrite /bindK; exact: funext_dep. Qed.
imports: mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib imonad_transformer