simp only [replaceFreeAux]
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ replaceFreeAux v t binders (def_ a✝¹ a✝) = fastReplaceFree v t (def_ a✝¹ a✝)
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ def_ a✝¹ (List.map (fun x => if v = x ∧ x ∉ binders then t else x) a✝) = fastReplaceFree v t (def_ a✝¹ a✝)