have thm₃ := BTheorem.mp (BTheorem.adj thm₂ thm₁) BTheorem.orE
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₂ ∈ Δ
lst₁ : List Form
l₆ : { x | x ∈ lst₁ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₃ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁} w₁
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₄ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂} w₂
thm₁ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁⊃w₁¦w₂)
thm₂ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂⊃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₂ ∈ Δ
lst₁ : List Form
l₆ : { x | x ∈ lst₁ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₃ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁} w₁
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₄ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂} w₂
thm₁ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁⊃w₁¦w₂)
thm₂ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂⊃w₁¦w₂)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          lst₂¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁⊃w₁¦w₂)
⊢ False