proposition: Lemma init_method_R: forall v1 v2, R v1 v2 -> RState _ _ R (init_method _ v1) (init_method _ v2).
proof: Proof. Proof using. intros. unfold RState. unfold init_method. simpl. split. intros. assumption. reflexivity. Qed.
imports: Coq(FunctionalExtensionality Arith List) Coq(Program.Equality ListSet Program.Basics Bool) Coq(Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs KVStore)