simp only [isFreeIn] at h1
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
h1 : ¬isFreeIn v (def_ a✝¹ a✝)
⊢ fastReplaceFree v t (def_ a✝¹ a✝) = def_ a✝¹ a✝
case def_
v t : VarName
a✝¹ : DefName
a✝ : List VarName
h1 : v ∉ a✝
⊢ fastReplaceFree v t (def_ a✝¹ a✝) = def_ a✝¹ a✝