split_ifs
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))
case pos
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
h✝ : v = x
⊢ ¬isFreeIn v (exists_ x phi)

case neg
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
h✝ : ¬v = x
⊢ ¬isFreeIn v (exists_ x (fastReplaceFree v t phi))