have ⟨⟨i,j⟩,l₂⟩ := finiteExhaustion lindenbaumSequenceMonotone l₁
t : Th
Δ : Ctx
f : Form
h₁ : lindenbaumExtension t Δ⊢f
prf₁ : BProof (lindenbaumExtension t Δ) f
s : Finset Form
l₁ : ↑s ⊆ lindenbaumExtension t Δ
fprf : BProof (↑s) f
⊢ f ∈ lindenbaumExtension t Δ
t : Th
Δ : Ctx
f : Form
h₁ : lindenbaumExtension t Δ⊢f
prf₁ : BProof (lindenbaumExtension t Δ) f
s : Finset Form
l₁ : ↑s ⊆ lindenbaumExtension t Δ
fprf : BProof (↑s) f
i j : ℕ
l₂ : ↑s ⊆ lindenbaumSequence t Δ (i, j)
⊢ f ∈ lindenbaumExtension t Δ