split at l₁
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
l₁ :
  w₁ ∈
    ▲match (i, j + 1) with
      | (0, 0) => ↑t
      | (Nat.succ i, 0) => { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) }
      | (i, Nat.succ j) =>
        let prev := lindenbaumSequence t Δ (i, j);
        let l := (Denumerable.ofNat (Form × Form) j).fst;
        let r := (Denumerable.ofNat (Form × Form) j).snd;
        if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
⊢ False
case h_1
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x✝ : Lex (ℕ × ℕ)
heq✝ : (i, j + 1) = (0, 0)
l₁ : w₁ ∈ ▲↑t
⊢ False

case h_2
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x✝ : Lex (ℕ × ℕ)
i✝ : ℕ
heq✝ : (i, j + 1) = (Nat.succ i✝, 0)
l₁ : w₁ ∈ ▲{ f | ∃ j, f ∈ lindenbaumSequence t Δ (i✝, j) }
⊢ False

case h_3
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x✝ : Lex (ℕ × ℕ)
i✝ j✝ : ℕ
heq✝ : (i, j + 1) = (i✝, Nat.succ j✝)
l₁ :
  w₁ ∈
    ▲let prev := lindenbaumSequence t Δ (i✝, j✝);
      let l := (Denumerable.ofNat (Form × Form) j✝).fst;
      let r := (Denumerable.ofNat (Form × Form) j✝).snd;
      if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
⊢ False