simp only [Function.updateITE_id]
case h.e'_2
x : VarName
phi : Formula
phi_ih : fastReplaceFree id phi = phi
⊢ fastReplaceFree (Function.updateITE id x x) phi = phi
case h.e'_2
x : VarName
phi : Formula
phi_ih : fastReplaceFree id phi = phi
⊢ fastReplaceFree id phi = phi