intros a h₁
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i : ℕ
⊢ ∀ (a : Lex (ℕ × ℕ)), a ≤ (i + 1, 0) → lindenbaumSequence t Δ a ⊆ lindenbaumSequence t Δ (i + 1, 0)
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i : ℕ
a : Lex (ℕ × ℕ)
h₁ : a ≤ (i + 1, 0)
⊢ lindenbaumSequence t Δ a ⊆ lindenbaumSequence t Δ (i + 1, 0)