simp only [isBoundIn] at h1
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : ¬isBoundIn u (def_ a✝¹ a✝)
h2 : u ∉ binders
⊢ fastAdmitsAux v u binders (def_ a✝¹ a✝)
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : ¬False
h2 : u ∉ binders
⊢ fastAdmitsAux v u binders (def_ a✝¹ a✝)