left
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 phi)
⊢ v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi
case h
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 phi)
⊢ v = x