cases h₁
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
a : Lex (ℕ × ℕ)
h₁ : a ≤ (i, j + 1)
⊢ lindenbaumSequence t Δ a ⊆ lindenbaumSequence t Δ (i, j + 1)
case left
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
a₁✝ b₁✝ : ℕ
h✝ : a₁✝ < i
⊢ lindenbaumSequence t Δ (a₁✝, b₁✝) ⊆ lindenbaumSequence t Δ (i, j + 1)

case right
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
b₁✝ : ℕ
h✝ : b₁✝ ≤ j + 1
⊢ lindenbaumSequence t Δ (i, b₁✝) ⊆ lindenbaumSequence t Δ (i, j + 1)