proposition: Lemma guard_method_R: forall n s1 s2 k v1 v2 u1 u2, RState _ _ R s1 s2 -> R v1 v2 -> RUpdate _ _ R u1 u2 -> guard_method _ n s1 k v1 u1 = guard_method _ n s2 k v2 u2.
proof: Proof. Proof using. intros. unfold guard_method. unfold RState in H. unfold RUpdate in H1. open_conjs. rewrite H1. rewrite H2. rewrite H3. reflexivity. Qed.
imports: Coq(FunctionalExtensionality List Bool Program.Basics) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs extralib KVStore)