case not_ phi phi_ih =>
  simp at h2
  exact phi_ih binders h1 h2
v u : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h2 : (toIsBoundAux binders phi).not_ = (toIsBoundAux binders (fastReplaceFree v u phi)).not_
⊢ fastAdmitsAux v u binders phi
no goals