have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp prf₅ thm₃⟩, l₅⟩
case nil.nil
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
l₆ l₇ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          []¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd []⊃w₁¦w₂)
⊢ False
case nil.nil
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
l₆ l₇ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          []¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd []⊃w₁¦w₂)
this : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ
⊢ False