∀ {m : Type u → Type v} {n : Type u → Type w} {inst : Monad m} {inst_1 : Monad n} {lift : ⦃α : Type u⦄ → m α → n α}
  [self : Std.Internal.LawfulMonadLiftFunction lift] {α β : Type u} (ma : m α) (f : α → m β),
  lift (ma >>= f) = do
    let x ← lift ma
    lift (f x)