have l₁ : ∀p : inst.primes, t ≤ p → p ⊨ f := by
  intros p h₂
  exact (h₁ p h₂).left
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
⊢ t⊨f
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f&g
l₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f
⊢ t⊨f