have l₁ : a₁ < i ∨ a₁ = i ∧ b₁ ≤ j := Or.inl h₂
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)
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
a₁ b₁ : ℕ
h₂ : a₁ < i
l₁ : a₁ < i ∨ a₁ = i ∧ b₁ ≤ j
⊢ lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i, j + 1)