proposition: Lemma node_nochange: forall (s s': State)(l: Label)(n': NId), let n := label_node l in let m := store (alg_state (node_states s n')) in let m' := store (alg_state (node_states s' n')) in (step s l s' /\ not (n = n')) -> m = m'.
proof: Proof. intros. open_conjs. inversion H; subst m; subst m'; subst s; subst s'; simpl; subst n; subst l; simpl in *; simpl_override; simpl_override; reflexivity. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)