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