dsimp at l₁ j
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
l₁ :
  w₁ ∈
    ▲let prev := lindenbaumSequence t Δ (i, Nat.add j 0);
      let l := (Denumerable.ofNat (Form × Form) (Nat.add j 0)).fst;
      let r := (Denumerable.ofNat (Form × Form) (Nat.add j 0)).snd;
      if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
⊢ False
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
l₁ :
  w₁ ∈
    ▲if
          (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
            ▲lindenbaumSequence t Δ (i, j + 0) then
        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}
      else lindenbaumSequence t Δ (i, j + 0)
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
⊢ False