case def_ =>
  simp only [Formula.primeSet] at h1
  simp at h1
  subst h1
  simp only [Formula.IsPrime]
F' : Formula
a✝¹ : DefName
a✝ : List VarName
h1 : F' ∈ (def_ a✝¹ a✝).primeSet
⊢ F'.IsPrime
no goals