intros f h₂
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i a₁ b₁ : ℕ
h₂ : a₁ < i + 1
l₁ : a₁ < i ∨ a₁ = i
l₂ : a₁ < i ∨ a₁ = i ∧ b₁ ≤ b₁
l₃ : ↑toLex (a₁, b₁) ≤ ↑toLex (i, b₁)
l₄ : lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i, b₁)
⊢ lindenbaumSequence t Δ (i, b₁) ≤ lindenbaumSequence t Δ (i + 1, 0)
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i a₁ b₁ : ℕ
h₂✝ : a₁ < i + 1
l₁ : a₁ < i ∨ a₁ = i
l₂ : a₁ < i ∨ a₁ = i ∧ b₁ ≤ b₁
l₃ : ↑toLex (a₁, b₁) ≤ ↑toLex (i, b₁)
l₄ : lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i, b₁)
f : Form
h₂ : f ∈ lindenbaumSequence t Δ (i, b₁)
⊢ f ∈ lindenbaumSequence t Δ (i + 1, 0)