case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  split_ifs
  case pos c1 =>
    congr! 1
    apply replaceFreeAux_mem_binders
    simp
    right
    exact c1
  case neg c1 =>
    congr! 1
    apply phi_ih
    simp
    tauto
v t x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∉ binders → replaceFreeAux v t binders phi = fastReplaceFree v t phi
binders : Finset VarName
h1 : v ∉ binders
⊢ exists_ x (replaceFreeAux v t (binders ∪ {x}) phi) =
    if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi)
no goals