rw [←l₁] at h₁
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
l₁ : ▲↑t = ↑t
⊢ ▲lindenbaumSequence t Δ (0, 0) ∩ Δ = ∅
t : Th
Δ : Ctx
h₁ : ▲↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
l₁ : ▲↑t = ↑t
⊢ ▲lindenbaumSequence t Δ (0, 0) ∩ Δ = ∅