proposition: Lemma map_update : forall A B (l:list A) (i:int) (x:A) (f:A->B), index l i -> map f (l[i := x]) = (map f l)[i := f x].
proof: Proof. Proof using. introv H. rewrite index_eq_inbound in H. unfold update_inst, update_impl, update. simpl. case_if. { false; math. } { applys LibList.map_update. { applys lt_nat_of_lt_int. rewrite abs_nonneg; math. } } Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)