proposition: Lemma step_star_not_in_nids: forall s ls s' n, step_star s ls s' -> ~List.In n nids -> prog (s n) = prog (s' n).
proof: Proof. Proof using max_nid_eq. intros. rewrite nids_eq in *. induction H using rev_step_star_ind; auto. rewrite <-IHstep_star; clear IHstep_star. inversion H; clear H; subst. * destruct (NId_eq_dec n0 n) as [Heq | Hneq]. rewrite !Heq in *. contradiction. simpl_override. reflexivity. * destruct (NId_eq_dec n0 n) as [Heq | Hneq]. rewrite !Heq in *. contradiction. simpl_override. reflexivity. * destruct (NId_eq_dec n n_1); destruct (NId_eq_dec n n_2); try subst; try contradiction; simpl_override; reflexivity. * destruct (NId_eq_dec n0 n) as [Heq | Hneq]. rewrite !Heq in *. contradiction. simpl_override. reflexivity. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)