simp only [fastReplaceFree]
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
⊢ ¬isFreeIn v (fastReplaceFree v t (exists_ x phi))
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
⊢ ¬isFreeIn v (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi))