have prf₃ : BProof (lindenbaumSequence t Δ ⟨i+1,Encodable.encode (f,f)⟩) (f ¦ f) := BProof.mp prf₂ BTheorem.orI₁
t : Th
Δ : Ctx
f : Form
h₁ : lindenbaumExtension t Δ⊢f
prf₁ : BProof (lindenbaumExtension t Δ) f
s : Finset Form
l₁ : ↑s ⊆ lindenbaumExtension t Δ
fprf : BProof (↑s) f
i j : ℕ
l₂ : ↑s ⊆ lindenbaumSequence t Δ (i, j)
l₃ : lindenbaumSequence t Δ (i, j) ⊆ lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
prf₂ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) f
⊢ f ∈ lindenbaumExtension t Δ
t : Th
Δ : Ctx
f : Form
h₁ : lindenbaumExtension t Δ⊢f
prf₁ : BProof (lindenbaumExtension t Δ) f
s : Finset Form
l₁ : ↑s ⊆ lindenbaumExtension t Δ
fprf : BProof (↑s) f
i j : ℕ
l₂ : ↑s ⊆ lindenbaumSequence t Δ (i, j)
l₃ : lindenbaumSequence t Δ (i, j) ⊆ lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
prf₂ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) f
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
⊢ f ∈ lindenbaumExtension t Δ