intros p h₃ h₄
α : Type
inst : Model α
s t : α
f : Form
h₁ : s ≤ t
g : Form
h₂ : s⊨~g
⊢ t⊨~g
α : Type
inst : Model α
s t : α
f : Form
h₁ : s ≤ t
g : Form
h₂ : s⊨~g
p : Model.primes
h₃ : t ≤ ↑p
h₄ : ↑(p*)⊨g
⊢ False