(motive : Lean.Level → Lean.Level → Sort u_1) →
  (u v : Lean.Level) →
    ((x : Lean.Level) → motive x Lean.Level.zero) →
      ((u v₁ v₂ : Lean.Level) → motive u (v₁.max v₂)) →
        ((u₁ u₂ v : Lean.Level) →
            (v = Lean.Level.zero → False) → (∀ (v₁ v₂ : Lean.Level), v = v₁.max v₂ → False) → motive (u₁.max u₂) v) →
          ((a u₂ v : Lean.Level) →
              (v = Lean.Level.zero → False) → (∀ (v₁ v₂ : Lean.Level), v = v₁.max v₂ → False) → motive (a.imax u₂) v) →
            ((u v : Lean.Level) → motive u.succ v.succ) →
              ((x x_1 : Lean.Level) →
                  (x_1 = Lean.Level.zero → False) →
                    (∀ (v₁ v₂ : Lean.Level), x_1 = v₁.max v₂ → False) →
                      (∀ (u₁ u₂ : Lean.Level), x = u₁.max u₂ → False) →
                        (∀ (a u₂ : Lean.Level), x = a.imax u₂ → False) →
                          (∀ (u v : Lean.Level), x = u.succ → x_1 = v.succ → False) → motive x x_1) →
                motive u v