proposition: Lemma get_nochange: forall (s s': State)(l: Label)(n: NId), let m := store (alg_state (node_states s n)) in let m' := store (alg_state (node_states s' n)) in (step s l s' /\ label_is_get l) -> m = m'.
proof: Proof. intros. open_conjs. inversion H. rewrite <- H3 in H0; unfold label_is_put in H0; inversion H0. subst m. subst m'. subst s. subst s'. simpl. unfold override. destruct (eq_nat_dec n n0). simpl. reflexivity. reflexivity. rewrite <- H4 in H0; unfold label_is_put in H0; inversion H0. rewrite <- H3 in H0; unfold label_is_put in H0; inversion H0. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)