case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  simp
  intro _
  exact phi_ih
v x : VarName
phi : Formula
phi_ih : fastReplaceFree v v phi = phi
⊢ (if v = x then exists_ x phi else exists_ x (fastReplaceFree v v phi)) = exists_ x phi
no goals