congr!
τ : PredName → PredName
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : phi.predVarSet = ∅
⊢ exists_ x (sub τ phi) = exists_ x phi
case h.e'_2
τ : PredName → PredName
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : phi.predVarSet = ∅
⊢ sub τ phi = phi