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