case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  congr!
  simp only [Function.updateITE_id]
  exact phi_ih
x : VarName
phi : Formula
phi_ih : fastReplaceFree id phi = phi
⊢ exists_ x (fastReplaceFree (Function.updateITE id x x) phi) = exists_ x phi
no goals