clear n m x heq₁ heq₂ h₃
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x : Lex (ℕ × ℕ)
n m : ℕ
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) ∩ Δ = ∅
heq₁ : i = n
heq₂ : Nat.add j 0 = m
⊢ False
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