simp only [replace]
P : PredName
zs : List VarName
H phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.predVarSet = ∅
⊢ replace P zs H phi.not_ = phi.not_
P : PredName
zs : List VarName
H phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.predVarSet = ∅
⊢ (replace P zs H phi).not_ = phi.not_