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))) /\ rec s1 = rec s2 /\ dep s1 = dep s2.
imports: Coq(FunctionalExtensionality List Bool Program.Basics) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs extralib KVStore)