unfold lindenbaumSequence
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
⊢ f ∈ lindenbaumSequence t Δ (i, j + 1)
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