simp
case h.h1
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 :
  BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) =
    toIsBoundAux binders (exists_ x (fastReplaceFree v u phi))
⊢ v ∉ binders ∪ {x}
case h.h1
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 :
  BoolFormula.forall_ (decide True) (toIsBoundAux (binders ∪ {x}) phi) =
    toIsBoundAux binders (exists_ x (fastReplaceFree v u phi))
⊢ v ∉ binders ∧ ¬v = x