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