intros p h₂ h₃
α : Type
inst : Model α
t : α
f✝ f : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨~f
⊢ t⊨~f
α : Type
inst : Model α
t : α
f✝ f : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨~f
p : Model.primes
h₂ : t ≤ ↑p
h₃ : ↑(p*)⊨f
⊢ False