split
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
⊢ f ∈
    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
case h_1
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
x✝ : Lex (ℕ × ℕ)
heq✝ : (i, j + 1) = (0, 0)
⊢ f ∈ ↑t

case h_2
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
x✝ : Lex (ℕ × ℕ)
i✝ : ℕ
heq✝ : (i, j + 1) = (Nat.succ i✝, 0)
⊢ f ∈ { f | ∃ j, f ∈ lindenbaumSequence t Δ (i✝, j) }

case h_3
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
x✝ : Lex (ℕ × ℕ)
i✝ j✝ : ℕ
heq✝ : (i, j + 1) = (i✝, Nat.succ j✝)
⊢ f ∈
    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