∀ (motive : Lean.Level → ℕ → Lean.Level → ℕ → Sort u_1) (l₁₁ l₁₂ : Lean.Level) (k₁ : ℕ) (l₂₁ l₂₂ : Lean.Level) (k₂ : ℕ)
  (h_1 : (l₁ : Lean.Level) → (k₁ : ℕ) → (l₂ : Lean.Level) → (k₂ : ℕ) → motive l₁.succ k₁ l₂ k₂)
  (h_2 : (l₁ : Lean.Level) → (k₁ : ℕ) → (l₂ : Lean.Level) → (k₂ : ℕ) → motive l₁ k₁ l₂.succ k₂)
  (h_3 :
    (l₁ l₁₁ l₁₂ : Lean.Level) →
      l₁ = l₁₁.max l₁₂ →
        (k₁ : ℕ) → (l₂ l₂₁ l₂₂ : Lean.Level) → l₂ = l₂₁.max l₂₂ → (k₂ : ℕ) → motive (l₁₁.max l₁₂) k₁ (l₂₁.max l₂₂) k₂)
  (h_4 :
    (l₁ l₁₁ l₁₂ : Lean.Level) →
      l₁ = l₁₁.imax l₁₂ →
        (k₁ : ℕ) →
          (l₂ l₂₁ l₂₂ : Lean.Level) → l₂ = l₂₁.imax l₂₂ → (k₂ : ℕ) → motive (l₁₁.imax l₁₂) k₁ (l₂₁.imax l₂₂) k₂)
  (h_5 :
    (n₁ : Lean.Name) →
      (k₁ : ℕ) → (n₂ : Lean.Name) → (k₂ : ℕ) → motive (Lean.Level.param n₁) k₁ (Lean.Level.param n₂) k₂)
  (h_6 :
    (n₁ : Lean.LMVarId) →
      (k₁ : ℕ) → (n₂ : Lean.LMVarId) → (k₂ : ℕ) → motive (Lean.Level.mvar n₁) k₁ (Lean.Level.mvar n₂) k₂)
  (h_7 : (l₁ : Lean.Level) → (k₁ : ℕ) → (l₂ : Lean.Level) → (k₂ : ℕ) → motive l₁ k₁ l₂ k₂),
  (match l₁₁.imax l₁₂, k₁, l₂₁.imax l₂₂, k₂ with
    | l₁.succ, k₁, l₂, k₂ => h_1 l₁ k₁ l₂ k₂
    | l₁, k₁, l₂.succ, k₂ => h_2 l₁ k₁ l₂ k₂
    | l₁@h:(l₁₁.max l₁₂), k₁, l₂@h_8:(l₂₁.max l₂₂), k₂ => h_3 l₁ l₁₁ l₁₂ h k₁ l₂ l₂₁ l₂₂ h_8 k₂
    | l₁@h:(l₁₁.imax l₁₂), k₁, l₂@h_8:(l₂₁.imax l₂₂), k₂ => h_4 l₁ l₁₁ l₁₂ h k₁ l₂ l₂₁ l₂₂ h_8 k₂
    | Lean.Level.param n₁, k₁, Lean.Level.param n₂, k₂ => h_5 n₁ k₁ n₂ k₂
    | Lean.Level.mvar n₁, k₁, Lean.Level.mvar n₂, k₂ => h_6 n₁ k₁ n₂ k₂
    | l₁, k₁, l₂, k₂ => h_7 l₁ k₁ l₂ k₂) =
    h_4 (l₁₁.imax l₁₂) l₁₁ l₁₂ ⋯ k₁ (l₂₁.imax l₂₂) l₂₁ l₂₂ ⋯ k₂