have l₂ : f ¦ g ∈ lindenbaumSequence t Δ ⟨i + 1, k⟩ := l₁ h₂
t : Th
Δ : Ctx
f g : Form
h₁ : f¦g ∈ lindenbaumExtension t Δ
i j : ℕ
h₂ : f¦g ∈ lindenbaumSequence t Δ (i, j)
k : ℕ := Encodable.encode (f, g)
l₁ : lindenbaumSequence t Δ (i, j) ⊆ lindenbaumSequence t Δ (i + 1, k)
⊢ f ∈ lindenbaumExtension t Δ ∨ g ∈ lindenbaumExtension t Δ
t : Th
Δ : Ctx
f g : Form
h₁ : f¦g ∈ lindenbaumExtension t Δ
i j : ℕ
h₂ : f¦g ∈ lindenbaumSequence t Δ (i, j)
k : ℕ := Encodable.encode (f, g)
l₁ : lindenbaumSequence t Δ (i, j) ⊆ lindenbaumSequence t Δ (i + 1, k)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
⊢ f ∈ lindenbaumExtension t Δ ∨ g ∈ lindenbaumExtension t Δ