unfold lindenbaumSequence
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
⊢ f ∈ lindenbaumSequence t Δ (i + 1, k + 1) ∨ g ∈ lindenbaumSequence t Δ (i + 1, k + 1)
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
⊢ (f ∈
      let prev := lindenbaumSequence t Δ (Nat.succ (Nat.add i 0), Nat.add k 0);
      let l := (Denumerable.ofNat (Form × Form) (Nat.add k 0)).fst;
      let r := (Denumerable.ofNat (Form × Form) (Nat.add k 0)).snd;
      if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev) ∨
    g ∈
      let prev := lindenbaumSequence t Δ (Nat.succ (Nat.add i 0), Nat.add k 0);
      let l := (Denumerable.ofNat (Form × Form) (Nat.add k 0)).fst;
      let r := (Denumerable.ofNat (Form × Form) (Nat.add k 0)).snd;
      if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev