proposition: Lemma bindA_uncurry (m : M A) (f : A -> M B) (g : A -> B -> M C) : (m >>= fun x => f x >>= fun y => Ret (x, y)) >>= (fun xy => g xy.1 xy.2) = (m >>= fun x => f x >>= g x).
proof: Proof. by rewrite bindA; by under eq_bind do rewrite bind_uncurry. Qed.
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy