{m : Type u → Type v} →
  {n : Type w → Type x} →
    [inst : Monad m] →
      [inst_1 : Monad n] →
        {liftBind : (γ : Type u) → (δ : Type w) → (γ → n δ) → m γ → n δ} →
          {motive : Std.Internal.LawfulMonadLiftBindFunction liftBind → Sort u_1} →
            (t : Std.Internal.LawfulMonadLiftBindFunction liftBind) →
              ((liftBind_pure : ∀ {γ : Type u} {δ : Type w} (f : γ → n δ) (a : γ), liftBind γ δ f (pure a) = f a) →
                  (liftBind_bind :
                      ∀ {β γ : Type u} {δ : Type w} (f : γ → n δ) (x : m β) (g : β → m γ),
                        liftBind γ δ f (x >>= g) = liftBind β δ (fun b => liftBind γ δ f (g b)) x) →
                    motive ⋯) →
                motive t