proposition: Lemma read_update_case : forall l i j v, index l j -> l[i:=v][j] = (If i = j then v else l[j]).
proof: Proof. Proof using. introv. unfold index_inst, index_impl, update_inst, update_impl, update, read_inst, read_impl. simpl. introv N. rewrite int_index_eq in N. case_if. math. case_if. case_if. auto. case_if. subst. rewrite~ nth_update_same. rewrite~ nth_update_neq. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)