exact ⟨⟨i + 1, Encodable.encode (f,f) + 1⟩, l₄⟩
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 Δ
no goals