case neg.mpr f => 
  intros p h₂ h₃
  rw [primeAnalysis] at h₁
  have l₁ : ~f ∈ p.val.val := (Set.mem_interₛ.mp h₁ p) ⟨p.property, h₂, p.val.property⟩
  exact canonicalSatisfaction.mp h₃ l₁
t : Th
f : Form
h₁ : ~f ∈ ↑t
⊢ t⊨~f
no goals