contrapose! h2
F : Formula
v u : VarName
binders : Finset VarName
h1 : fastAdmitsAux v u binders F
h2 : u ∈ binders
⊢ ¬isFreeIn v F
F : Formula
v u : VarName
binders : Finset VarName
h1 : fastAdmitsAux v u binders F
h2 : isFreeIn v F
⊢ u ∉ binders