fact: Definition CacheADTwLogIndex_AbsR (or : Ensemble (Key * Value)) (nr : Ensemble (Key * Value) * Ensemble (Key * nat)) := or = (fst nr) /\ (KVEnsemble_EquivalentKeys (fst nr) (snd nr)).
imports: Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Computation ADT ADTRefinement ADTNotation BuildADTRefinements KVEnsembles CacheSpec