have l₃ : f ∈ lindenbaumSequence t Δ ⟨i + 1, k + 1⟩ ∨ g ∈ lindenbaumSequence t Δ ⟨i + 1, k + 1⟩ := by
  unfold lindenbaumSequence
  change
    let prev := lindenbaumSequence t Δ (i + 1, k);
    let l := (Denumerable.ofNat (Form × Form) k).fst;
    let r := (Denumerable.ofNat (Form × Form) k).snd;
    (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)
  intros prev l r
  have l₄ : Denumerable.ofNat (Form × Form) k = (f,g) := Denumerable.ofNat_encode (f,g)
  have l₅ : l = f := by 
    change (Denumerable.ofNat (Form × Form) k).fst = f
    rw [l₄]
  have l₆ : r = g := by 
    change (Denumerable.ofNat (Form × Form) k).snd = g
    rw [l₄]
  repeat rw [l₅,l₆]
  clear l r l₅ l₆
  cases Classical.em (▲(prev ∪ {f}) ∩ Δ = ∅)
  case' inl h₁ => apply Or.inl
  case' inr h₁ => apply Or.inr
  all_goals
    split
    case inl => exact Or.inr rfl
    case inr h₂ => exact False.elim $ h₂ ⟨BProof.ax l₂⟩
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
⊢ f ∈ lindenbaumExtension t Δ ∨ g ∈ lindenbaumExtension t Δ
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
l₃ : f ∈ lindenbaumSequence t Δ (i + 1, k + 1) ∨ g ∈ lindenbaumSequence t Δ (i + 1, k + 1)
⊢ f ∈ lindenbaumExtension t Δ ∨ g ∈ lindenbaumExtension t Δ