have l₁ := @h₁ pr h₂.right.left
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) }
⊢ ~f ∈ p
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
⊢ ~f ∈ p