exact l₂
case h
t : Th
f : Form
h₁ : t⊨~f
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
l₁ : ¬↑(pr*)⊨f
l₂ : f ∈ ↑↑(pr*) → False
⊢ ¬~f ∈ p → False
no goals