congr!
x : VarName
phi : Formula
phi_ih : fastReplaceFree id phi = phi
⊢ exists_ x (fastReplaceFree (Function.updateITE id x x) phi) = exists_ x phi
case h.e'_2
x : VarName
phi : Formula
phi_ih : fastReplaceFree id phi = phi
⊢ fastReplaceFree (Function.updateITE id x x) phi = phi