{motive : Lean.Level → Sort u} →
  (t : Lean.Level) →
    motive Lean.Level.zero →
      ((a : Lean.Level) → motive a.succ) →
        ((a a_1 : Lean.Level) → motive (a.max a_1)) →
          ((a a_1 : Lean.Level) → motive (a.imax a_1)) →
            ((a : Lean.Name) → motive (Lean.Level.param a)) →
              ((a : Lean.LMVarId) → motive (Lean.Level.mvar a)) → motive t