fact: Definition RState (Val1: Type)(Val2: Type)(R: Val1 -> Val2 -> Prop)(s1: @State Val1)(s2: @State Val2): Prop := (forall k, R (entry_val (store s1 k)) (entry_val (store s2 k)) /\ (entry_node (store s1 k)) = (entry_node (store s2 k)) /\ (entry_clock (store s1 k)) = (entry_clock (store s2 k))) /\ received s1 = received s2 /\ clock s1 = clock s2 /\ dep s1 = dep s2.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)