unfold satisfies at h₂
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : p*⊨f
h₂ : ↑p⊨~f
⊢ False
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : p*⊨f
h₂ : ∀ {p_1 : Model.primes}, ↑p ≤ ↑p_1 → ¬↑(p_1*)⊨f
⊢ False