proposition: Lemma liftM2E m1 m2 D (f : C -> M D) : liftM2 h m1 m2 >>= f = m1 >>= (fun x => m2 >>= fun y => f (h x y)) :> M _.
proof: Proof. rewrite /liftM2 bindA; under eq_bind do rewrite bindA. by bind_ext => s; under eq_bind do rewrite bindretf. Qed.
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy