proposition: Lemma update_cons_case : forall x l i z, index (x::l) i -> (x::l)[i:=z] = If i = 0 then z::l else x::(l[i-1:=z]).
proof: Proof. Proof using. introv H. case_if. { subst. rewrite* update_zero. } { rewrite* update_cons_pos. rew_index in H. math. } Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)