rw [Nat.le_zero_eq b₁] at h₂
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i b₁ : ℕ
h₂ : b₁ ≤ 0
⊢ lindenbaumSequence t Δ (i + 1, b₁) ⊆ lindenbaumSequence t Δ (i + 1, 0)
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i b₁ : ℕ
h₂ : b₁ = 0
⊢ lindenbaumSequence t Δ (i + 1, b₁) ⊆ lindenbaumSequence t Δ (i + 1, 0)