proposition: Lemma update_set_nth : forall r x v r', s_update r x v r' -> set_nth (env_to_mem r) (symbol_index (map fst r) x) v = (env_to_mem r').
proof: Proof. induction 1 as [env x v v' | env env' x y v v' upd Ih xny]. simpl. now destruct (S.string_dec x x) as [_ | abs];[ | now case abs]. simpl. destruct (S.string_dec x y) as [abs | _];[ now case xny |]. now rewrite Ih. Qed.
imports: ZArith Arith List syntax little Lia