congr!
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_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ (replace P zs H phi).iff_ (replace P zs H psi) = phi.iff_ psi
case h.e'_1
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_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ replace P zs H phi = phi

case h.e'_2
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_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ replace P zs H psi = psi