proposition: Lemma update_index r x v r' : s_update r x v r' -> map fst r = map fst r'.
proof: Proof. induction 1 as [r x v v' | r r' x y v v' up Ih xny]. easy. now simpl; rewrite Ih. Qed.
imports: ZArith Arith List syntax little Lia