simp at h1
F' : Formula
a✝ : VarName
x : Formula
phi : F' ∈ x.primeSet → F'.IsPrime
h1 : F' ∈ {exists_ a✝ x}
⊢ F'.IsPrime
F' : Formula
a✝ : VarName
x : Formula
phi : F' ∈ x.primeSet → F'.IsPrime
h1 : F' = exists_ a✝ x
⊢ F'.IsPrime