case inl h₄ =>
  split at l₁
  case inl h₅ => exact (Set.not_nonempty_iff_eq_empty.mpr h₅) ⟨w₁, l₁, l₂⟩
  case inr h₅ =>
    have ⟨prf₁⟩ := l₁
    have ⟨w₂,⟨⟨prf₂⟩,l₄⟩⟩ := Set.nonempty_iff_ne_empty.mpr h₅
    have l₅ : w₁¦w₂ ∈ Δ := h₂ ⟨l₂, l₄⟩
    clear l₁ l₂ l₄ h₅
    have ⟨lst₁,l₆,prf₃⟩ := BProof.sentenceCompactness (Set.union_singleton ▸ prf₁)
    have ⟨lst₂,l₇,prf₄⟩ := BProof.sentenceCompactness (Set.union_singleton ▸ prf₂)
    have thm₁ := BTheorem.transitivity prf₃.toTheorem (BTheorem.orI₁ : BTheorem (w₁ ⊃ w₁ ¦ w₂))
    have thm₂ := BTheorem.transitivity prf₄.toTheorem (BTheorem.orI₂ : BTheorem (w₂ ⊃ w₁ ¦ w₂))
    have thm₃ := BTheorem.mp (BTheorem.adj thm₂ thm₁) BTheorem.orE 
    have ⟨prf₅⟩ := h₄
    clear h₄ thm₁ thm₂ prf₁ prf₂ prf₃ prf₄
    cases lst₁
    all_goals 
      cases lst₂
    case' nil.nil =>
      have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp prf₅ thm₃⟩, l₅⟩
      exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
    case' nil.cons head tail =>
      have := BProof.proveList l₇
      have := BProof.mp (BProof.adj prf₅ this) BTheorem.distRight
      have := BProof.mp this (BTheorem.orFunctor BTheorem.taut BTheorem.andE₁)
      have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp this thm₃⟩, l₅⟩
      exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
    case' cons.nil head tail => 
      have := BProof.proveList l₆
      have := BProof.mp (BProof.adj prf₅ this) BTheorem.distRight
      have := BProof.mp this (BTheorem.orFunctor BTheorem.andE₁ BTheorem.taut)
      have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp this thm₃⟩, l₅⟩
      exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
    case' cons.cons head tail head' tail'=> 
      have prf₆ := BProof.proveList l₆
      have prf₇ := BProof.proveList l₇
      have := BProof.mp (BProof.adj prf₅ prf₇) BTheorem.distRight
      have prf₈ := BProof.mp this (BTheorem.orFunctor BTheorem.taut BTheorem.andE₁)
      have := BProof.mp (BProof.adj prf₈ prf₆) BTheorem.distRight
      have prf₉ := BProof.mp this (BTheorem.orFunctor BTheorem.andE₁ BTheorem.taut)
      have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp prf₉ thm₃⟩, l₅⟩
      exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
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)
l₁ :
  w₁ ∈
    ▲if ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅ then
        lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}
      else lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}
⊢ False
no goals