push_neg at h1
v t x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName), ¬occursIn t phi → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t phi)
binders : Finset VarName
h1 : ¬(t = x ∨ occursIn t phi)
h2 : v ∉ binders
⊢ fastAdmitsAux t v binders (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi))
v t x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName), ¬occursIn t phi → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t phi)
binders : Finset VarName
h2 : v ∉ binders
h1 : t ≠ x ∧ ¬occursIn t phi
⊢ fastAdmitsAux t v binders (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi))