exact upwardsClosure l₄ l₅
case h₁
α : Type
inst : Model α
t : α
f✝ f g : Form
h₁ : ∀ (p : Model.primes), t ≤ ↑p → p⊨f⊃g
u : α
h₂ : u⊨f
p : Model.primes
h₃ : t∙u ≤ ↑p
q w✝ : Subtype Model.prime
l₃ : t ≤ ↑q
left✝ : u ≤ ↑w✝
l₄ : ↑q∙u ≤ ↑p
right✝ : t∙↑w✝ ≤ ↑p
l₅ : ↑q∙u⊨g
⊢ p⊨g
no goals