exact h2
case h.h2
v u x : 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
c1 : ¬v = x
h2 : toIsBoundAux (binders ∪ {x}) phi = toIsBoundAux (binders ∪ {x}) (fastReplaceFree v u phi)
⊢ toIsBoundAux (binders ∪ {x}) phi = toIsBoundAux (binders ∪ {x}) (fastReplaceFree v u phi)
no goals