intros f h₃
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
⊢ lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
⊢ f ∈ lindenbaumSequence t Δ (i, j + 1)