unfold lindenbaumExtension
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
⊢ lindenbaumExtension t Δ ∩ Δ = ∅
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
⊢ { f | ∃ ij, f ∈ lindenbaumSequence t Δ ij } ∩ Δ = ∅