have l₅ : l = f := by 
  change (Denumerable.ofNat (Form × Form) k).fst = f
  rw [l₄]
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
prev : Ctx := lindenbaumSequence t Δ (i + 1, k)
l : Form := (Denumerable.ofNat (Form × Form) k).fst
r : Form := (Denumerable.ofNat (Form × Form) k).snd
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
⊢ (f ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev) ∨
    g ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
prev : Ctx := lindenbaumSequence t Δ (i + 1, k)
l : Form := (Denumerable.ofNat (Form × Form) k).fst
r : Form := (Denumerable.ofNat (Form × Form) k).snd
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
l₅ : l = f
⊢ (f ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev) ∨
    g ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev