apply phi_ih
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), fastAdmitsAux v u binders phi → admitsAux v u binders phi
binders : Finset VarName
h1 : fastAdmitsAux v u (binders ∪ {x}) phi
⊢ admitsAux v u (binders ∪ {x}) phi
case h1
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), fastAdmitsAux v u binders phi → admitsAux v u binders phi
binders : Finset VarName
h1 : fastAdmitsAux v u (binders ∪ {x}) phi
⊢ fastAdmitsAux v u (binders ∪ {x}) phi