fact: Definition update_impl A (l:list A) (i:int) (v:A) : list A := If i < 0 then l else LibList.update (abs i) v l.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)