cases h1
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), fastAdmitsAux v u binders phi → isFreeIn v phi → u ∉ binders
binders : Finset VarName
h1 : v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi
h2_left : ¬v = x
h2_right : isFreeIn v phi
⊢ u ∉ binders
case inl
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), fastAdmitsAux v u binders phi → isFreeIn v phi → u ∉ binders
binders : Finset VarName
h2_left : ¬v = x
h2_right : isFreeIn v phi
h✝ : v = x
⊢ u ∉ binders

case inr
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), fastAdmitsAux v u binders phi → isFreeIn v phi → u ∉ binders
binders : Finset VarName
h2_left : ¬v = x
h2_right : isFreeIn v phi
h✝ : fastAdmitsAux v u (binders ∪ {x}) phi
⊢ u ∉ binders