fact: Definition init_method (init_val: Val): State := state (fun (k: Key) => entry init_val 0 0) (fun (n: NId) => 0) (fun (n: NId) => 0).
imports: Coq(FunctionalExtensionality List Bool Program.Basics) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs extralib KVStore)