fact: Definition RUpdate (Val1: Type)(Val2: Type)(R: Val1 -> Val2 -> Prop)(u1: @Update Val1)(u2: @Update Val2): Prop := sender_node u1 = sender_node u2 /\ sender_clock u1 = sender_clock u2 /\ sender_dep u1 = sender_dep u2.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)