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