have ⟨x, l₁⟩ := nonconstruction h₁
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : ¬p⊨~f
⊢ p*⊨f
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : ¬p⊨~f
x : Model.primes
l₁ : ¬(↑p ≤ ↑x → ¬↑(x*)⊨f)
⊢ p*⊨f