simp only [admitsAux] at h1
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : admitsAux v u binders (def_ a✝¹ a✝)
h2 : isFreeIn v (def_ a✝¹ a✝)
h3 : v ∉ binders
⊢ u ∉ binders
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∈ a✝ ∧ v ∉ binders → u ∉ binders
h2 : isFreeIn v (def_ a✝¹ a✝)
h3 : v ∉ binders
⊢ u ∉ binders