simp
case h1
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), admitsAux v u binders phi → isFreeIn v phi → v ∉ binders → u ∉ binders
binders : Finset VarName
h1 : admitsAux v u (binders ∪ {x}) phi
h3 : v ∉ binders
h2_left : ¬v = x
h2_right : isFreeIn v phi
⊢ v ∉ {x}
case h1
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), admitsAux v u binders phi → isFreeIn v phi → v ∉ binders → u ∉ binders
binders : Finset VarName
h1 : admitsAux v u (binders ∪ {x}) phi
h3 : v ∉ binders
h2_left : ¬v = x
h2_right : isFreeIn v phi
⊢ ¬v = x