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

case right
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
b₁✝ : ℕ
h✝ : b₁✝ ≤ 0
⊢ lindenbaumSequence t Δ (0, b₁✝) ⊆ lindenbaumSequence t Δ (0, 0)