cases l₁
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i a₁ b₁ : ℕ
h₂ : a₁ < i + 1
l₁ : a₁ < i ∨ a₁ = i
⊢ a₁ < i ∨ a₁ = i ∧ b₁ ≤ b₁
case inl
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i a₁ b₁ : ℕ
h₂ : a₁ < i + 1
h✝ : a₁ < i
⊢ a₁ < i ∨ a₁ = i ∧ b₁ ≤ b₁

case inr
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i a₁ b₁ : ℕ
h₂ : a₁ < i + 1
h✝ : a₁ = i
⊢ a₁ < i ∨ a₁ = i ∧ b₁ ≤ b₁