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