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