case not_ phi phi_ih =>
  simp only [predVarSet] at h1
  simp only [replace]
  congr!
  exact phi_ih h1
P : PredName
zs : List VarName
H phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.not_.predVarSet = ∅
⊢ replace P zs H phi.not_ = phi.not_
no goals