simp only [toIsBoundAux]
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      fastAdmitsAux v u binders phi → toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi)
binders : Finset VarName
h1 : v ∉ binders
h2 : v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
⊢ BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) =
    toIsBoundAux binders (exists_ x (fastReplaceFree v u phi))
v u x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      fastAdmitsAux v u binders phi → toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi)
binders : Finset VarName
h1 : v ∉ binders
h2 : v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
⊢ BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) =
    BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) (fastReplaceFree v u phi))