proposition: Lemma update_same : forall (IA:Inhab A) l i, index l i -> l[i:=l[i]] = l.
proof: Proof. Proof using. intros IA l. induction l; intros i Hi. { rew_index in Hi. rew_list in Hi. false. math. } { rew_index in *. rewrite* update_cons_case. case_if. { fequals. subst. rewrite* read_zero. } { fequals. rewrite* read_cons_pos. math. } } Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)