proposition: Lemma update_method_R: forall n s1 s2 k v1 v2 u1 u2, RState _ _ R s1 s2 -> R v1 v2 -> RUpdate _ _ R u1 u2 -> RState _ _ R (update_method _ n s1 k v1 u1) (update_method _ n s2 k v2 u2).
proof: Proof. Proof using. intros. unfold RState. unfold update_method. simpl. unfold RState in H. unfold RUpdate in H1. open_conjs. split_all. intros. destruct (eq_nat_dec k k0). simpl_override. simpl_override. split_all; assumption. simpl_override. simpl_override. specialize (H k0). open_conjs. split_all; assumption. rewrite H1. rewrite H2. rewrite H4. reflexivity. assumption. assumption. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)