clear l₁ l₂ l₄ h₅
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
h₅ : ¬▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅
l₁ : w₁ ∈ ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd})
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
w₂ : Form
prf₂ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) w₂
l₄ : w₂ ∈ Δ
l₅ : w₁¦w₂ ∈ Δ
⊢ False
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
w₂ : Form
prf₂ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) w₂
l₅ : w₁¦w₂ ∈ Δ
⊢ False