have l₄ : f ∈ lindenbaumSequence t Δ ⟨i + 1, Encodable.encode (f,f) + 1⟩ := by
  unfold lindenbaumSequence
  change
    let prev := lindenbaumSequence t Δ (i + 1, Encodable.encode (f,f));
    let l := (Denumerable.ofNat (Form × Form) (Encodable.encode (f,f))).fst;
    let r := (Denumerable.ofNat (Form × Form) (Encodable.encode (f,f))).snd;
    f ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
  intros prev l r
  have l₅ : l = f := by 
    change (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst = f
    rw [Denumerable.ofNat_encode (f,f)]
  have l₆ : r = f := by
    change (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd = f
    rw [Denumerable.ofNat_encode (f,f)]
  split
  case inl h₂ =>
    split
    . rw [l₅]; exact Or.inr rfl
    . rw [l₆]; exact Or.inr rfl
  case inr h₂ =>
    apply False.elim
    have l₇ : f¦f ∈ ▲prev := ⟨prf₃⟩
    rw [l₅,l₆] at h₂
    exact h₂ l₇
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
⊢ f ∈ lindenbaumExtension t Δ
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
l₄ : f ∈ lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f) + 1)
⊢ f ∈ lindenbaumExtension t Δ