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