simp only [Formula.primeSet] at h1
F' : Formula
a✝¹ : DefName
a✝ : List VarName
h1 : F' ∈ (def_ a✝¹ a✝).primeSet
⊢ F'.IsPrime
F' : Formula
a✝¹ : DefName
a✝ : List VarName
h1 : F' ∈ {def_ a✝¹ a✝}
⊢ F'.IsPrime