case neg.mp f => 
  rw [primeAnalysis]
  intros p h₂
  let pr : Pr := ⟨⟨p, h₂.right.right⟩,h₂.left⟩
  have l₁ := @h₁ pr h₂.right.left
  have l₂ := l₁ ∘ canonicalSatisfaction.mpr 
  apply byContradiction
  exact l₂
t : Th
f : Form
h₁ : t⊨~f
⊢ ~f ∈ ↑t
no goals