change
  ▲{ f : Form | ∃j : Nat, f ∈ lindenbaumSequence t Δ ⟨i, j⟩ } ∩ Δ = ∅
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
⊢ ▲lindenbaumSequence t Δ (i + 1, 0) ∩ Δ = ∅
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
⊢ ▲{ f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } ∩ Δ = ∅