case pos c1 =>
  congr! 1
  apply replaceFreeAux_mem_binders
  simp
  right
  exact c1
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
c1 : v = x
⊢ exists_ x (replaceFreeAux v t (binders ∪ {x}) phi) = exists_ x phi
no goals