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