proposition: Lemma read_update_neq : forall l i j v, index l j -> (i <> j) -> (l[i:=v])[j] = l[j].
proof: Proof. Proof using. introv N. rewrite~ read_update_case. case_if; auto_false~. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)