∀ (_x : (_ : Lean.Level) ×' (_ : ℕ) ×' (_ : Lean.Level) ×' ℕ),
  Lean.Level.normLtAux._unary _x =
    PSigma.casesOn _x fun a a_1 =>
      PSigma.casesOn a_1 fun a_2 a_3 =>
        PSigma.casesOn a_3 fun a_4 a_5 =>
          match a, a_2, a_4, a_5 with
          | l₁.succ, k₁, l₂, k₂ => Lean.Level.normLtAux._unary ⟨l₁, ⟨k₁ + 1, ⟨l₂, k₂⟩⟩⟩
          | l₁, k₁, l₂.succ, k₂ => Lean.Level.normLtAux._unary ⟨l₁, ⟨k₁, ⟨l₂, k₂ + 1⟩⟩⟩
          | l₁@h:(l₁₁.max l₁₂), k₁, l₂@h_1:(l₂₁.max l₂₂), k₂ =>
            if (l₁ == l₂) = true then decide (k₁ < k₂)
            else
              if (l₁₁ != l₂₁) = true then Lean.Level.normLtAux._unary ⟨l₁₁, ⟨0, ⟨l₂₁, 0⟩⟩⟩
              else Lean.Level.normLtAux._unary ⟨l₁₂, ⟨0, ⟨l₂₂, 0⟩⟩⟩
          | l₁@h:(l₁₁.imax l₁₂), k₁, l₂@h_1:(l₂₁.imax l₂₂), k₂ =>
            if (l₁ == l₂) = true then decide (k₁ < k₂)
            else
              if (l₁₁ != l₂₁) = true then Lean.Level.normLtAux._unary ⟨l₁₁, ⟨0, ⟨l₂₁, 0⟩⟩⟩
              else Lean.Level.normLtAux._unary ⟨l₁₂, ⟨0, ⟨l₂₂, 0⟩⟩⟩
          | Lean.Level.param n₁, k₁, Lean.Level.param n₂, k₂ => if (n₁ == n₂) = true then decide (k₁ < k₂) else n₁.lt n₂
          | Lean.Level.mvar n₁, k₁, Lean.Level.mvar n₂, k₂ =>
            if (n₁ == n₂) = true then decide (k₁ < k₂) else n₁.name.lt n₂.name
          | l₁, k₁, l₂, k₂ => if (l₁ == l₂) = true then decide (k₁ < k₂) else decide (l₁.ctorToNat < l₂.ctorToNat)