proposition: Lemma bindretf : BindLaws.left_neutral (@bind M) ret.
proof: Proof. move: (@bindretf_derived M ret join joinretM). 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)