simp only [fastReplaceFree]
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1_left : t ≠ x
h1_right : ¬occursIn t phi
c1 : ¬v = x
⊢ fastReplaceFree t v (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_left : t ≠ x
h1_right : ¬occursIn t phi
c1 : ¬v = x
⊢ (if t = x then exists_ x (fastReplaceFree v t phi) else exists_ x (fastReplaceFree t v (fastReplaceFree v t phi))) =
    exists_ x phi