case forall_ x phi | exists_ x phi =>
  simp only [Formula.primeSet] at h1
  simp at h1
  subst h1
  simp only [Formula.IsPrime]
F' : Formula
a✝ : VarName
x : Formula
phi : F' ∈ x.primeSet → F'.IsPrime
h1 : F' ∈ (exists_ a✝ x).primeSet
⊢ F'.IsPrime
no goals