by_cases c1 : v = x
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∉ binders → admitsAux v u binders phi → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h2 : admitsAux v u (binders ∪ {x}) phi
⊢ v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi
case pos
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∉ binders → admitsAux v u binders phi → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h2 : admitsAux v u (binders ∪ {x}) phi
c1 : v = x
⊢ v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi

case neg
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∉ binders → admitsAux v u binders phi → fastAdmitsAux v u binders phi
binders : Finset VarName
h1 : v ∉ binders
h2 : admitsAux v u (binders ∪ {x}) phi
c1 : ¬v = x
⊢ v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi