fact: Record StateRec {Val: Type} := { store: Key -> @Entry Val; rec: NId -> Clock; dep: NId -> Clock }.
imports: Coq(FunctionalExtensionality List Bool Program.Basics) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs extralib KVStore)