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. split_all. assumption. reflexivity. reflexivity. split_all; reflexivity. Qed.
imports: Coq(FunctionalExtensionality List Bool Program.Basics) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs extralib KVStore)