congr!
P : PredName
zs : List VarName
H : Formula
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.predVarSet = ∅
⊢ exists_ x (replace P zs H phi) = exists_ x phi
case h.e'_2
P : PredName
zs : List VarName
H : Formula
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → replace P zs H phi = phi
h1 : phi.predVarSet = ∅
⊢ replace P zs H phi = phi