intros u h₂
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f⊃g
⊢ t⊨f⊃g
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f⊃g
u : α
h₂ : u⊨f
⊢ t∙u⊨g