simp only [fastAdmitsAux]
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ fastAdmitsAux v v binders (def_ a✝¹ a✝)
case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ v ∈ a✝ → v ∉ binders