fact: Definition cache_inv_Property (P : CacheDecode -> Prop) (P_inv : (CacheDecode -> Prop) -> Prop) := P_inv P.
imports: Coq.Lists.List Fiat.Common Fiat.Computation.Core Fiat.Computation.Notations Fiat.Narcissus.Common.Notations Fiat.Narcissus.Common.Monoid Fiat.Narcissus.Stores.Cache