push_neg at h1
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1 : ¬(t = x ∨ occursIn t phi)
⊢ fastReplaceFree t v (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi)) = exists_ x phi
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1 : t ≠ x ∧ ¬occursIn t phi
⊢ fastReplaceFree t v (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi)) = exists_ x phi