∀ (motive : Lean.Level → Lean.Level → Sort u_1) (a : Lean.Level)
  (h_1 : (u v : Lean.Name) → motive (Lean.Level.param u) (Lean.Level.param v))
  (h_2 : Unit → motive Lean.Level.zero Lean.Level.zero) (h_3 : (u v : Lean.Level) → motive u.succ v.succ)
  (h_4 : (a : Lean.Level) → motive Lean.Level.zero a.succ) (h_5 : (a : Lean.Level) → motive a.succ Lean.Level.zero)
  (h_6 : (v₁ v₂ : Lean.Level) → motive Lean.Level.zero (v₁.max v₂))
  (h_7 : (u₁ u₂ : Lean.Level) → motive (u₁.max u₂) Lean.Level.zero)
  (h_8 : (a v : Lean.Level) → motive Lean.Level.zero (a.imax v))
  (h_9 : (a u : Lean.Level) → motive (a.imax u) Lean.Level.zero)
  (h_10 : (u₁ u₂ v₁ v₂ : Lean.Level) → motive (u₁.max u₂) (v₁.max v₂))
  (h_11 : (u₁ u₂ v₁ v₂ : Lean.Level) → motive (u₁.imax u₂) (v₁.imax v₂)) (h_12 : (x x_1 : Lean.Level) → motive x x_1),
  (match Lean.Level.zero, a.succ with
    | Lean.Level.param u, Lean.Level.param v => h_1 u v
    | Lean.Level.zero, Lean.Level.zero => h_2 ()
    | u.succ, v.succ => h_3 u v
    | Lean.Level.zero, a.succ => h_4 a
    | a.succ, Lean.Level.zero => h_5 a
    | Lean.Level.zero, v₁.max v₂ => h_6 v₁ v₂
    | u₁.max u₂, Lean.Level.zero => h_7 u₁ u₂
    | Lean.Level.zero, a.imax v => h_8 a v
    | a.imax u, Lean.Level.zero => h_9 a u
    | u₁.max u₂, v₁.max v₂ => h_10 u₁ u₂ v₁ v₂
    | u₁.imax u₂, v₁.imax v₂ => h_11 u₁ u₂ v₁ v₂
    | x, x_1 => h_12 x x_1) =
    h_4 a