{m : Type → Type v} →
  {motive : Lean.Server.MonadCancellable m → Sort u} →
    (t : Lean.Server.MonadCancellable m) →
      ((checkCancelled : m PUnit.{1}) → motive { checkCancelled := checkCancelled }) → motive t