fact: Definition cachedRep_AbsR (or : rep) (nr : cachedRep) := or = origRep nr /\ cacheSpec or (cachedVal nr).
imports: Fiat.Common Fiat.Computation Fiat.ADT Coq.Sets.Ensembles Fiat.ADTRefinement Fiat.ADTRefinement.Refinements.ADTRepInv