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