have l₄ := lindenbaumAvoids h₁ h₂ ⟨i,j⟩
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
w : Form
prf₁ : BProof { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } w
l₁ : w ∈ Δ
s : Finset Form
l₂ : ↑s ⊆ { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) }
prf₂ : BProof (↑s) w
j : ℕ
l₃ : ↑s ⊆ lindenbaumSequence t Δ (i, j)
⊢ False
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
w : Form
prf₁ : BProof { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } w
l₁ : w ∈ Δ
s : Finset Form
l₂ : ↑s ⊆ { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) }
prf₂ : BProof (↑s) w
j : ℕ
l₃ : ↑s ⊆ lindenbaumSequence t Δ (i, j)
l₄ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
⊢ False