case h_1 x heq => injection heq with heq; contradiction
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x : Lex (ℕ × ℕ)
heq : (i, j + 1) = (0, 0)
l₁ : w₁ ∈ ▲↑t
⊢ False
no goals