(motive : Lean.Level → Lean.Level → Sort u_1) →
  (u v : Lean.Level) →
    ((u v : Lean.Name) → motive (Lean.Level.param u) (Lean.Level.param v)) →
      (Unit → motive Lean.Level.zero Lean.Level.zero) →
        ((u v : Lean.Level) → motive u.succ v.succ) →
          ((a : Lean.Level) → motive Lean.Level.zero a.succ) →
            ((a : Lean.Level) → motive a.succ Lean.Level.zero) →
              ((v₁ v₂ : Lean.Level) → motive Lean.Level.zero (v₁.max v₂)) →
                ((u₁ u₂ : Lean.Level) → motive (u₁.max u₂) Lean.Level.zero) →
                  ((a v : Lean.Level) → motive Lean.Level.zero (a.imax v)) →
                    ((a u : Lean.Level) → motive (a.imax u) Lean.Level.zero) →
                      ((u₁ u₂ v₁ v₂ : Lean.Level) → motive (u₁.max u₂) (v₁.max v₂)) →
                        ((u₁ u₂ v₁ v₂ : Lean.Level) → motive (u₁.imax u₂) (v₁.imax v₂)) →
                          ((x x_1 : Lean.Level) → motive x x_1) → motive u v