fact: Record UpdateRec {Val: Type} := { sender_node: NId; sender_clock: NId -> Clock }.
imports: Coq(FunctionalExtensionality Arith List) Coq(Program.Equality ListSet Program.Basics Bool) Coq(Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs KVStore)