fact: Record UpdateRec {Val: Type} := { sender_node: NId; sender_clock: Clock; sender_dep: list (NId * Clock) }.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)