simp
v x : VarName
phi : Formula
phi_ih : fastReplaceFree v v phi = phi
⊢ (if v = x then exists_ x phi else exists_ x (fastReplaceFree v v phi)) = exists_ x phi
v x : VarName
phi : Formula
phi_ih : fastReplaceFree v v phi = phi
⊢ ¬v = x → fastReplaceFree v v phi = phi