fact: Definition CorrectAlignedDecoder {S : Type} (predicate : S -> Prop) (format : FormatM S ByteString) (decoder : forall sz, AlignedDecodeM S sz) := {decodePlusCacheInv : _ & (exists P_inv : (CacheDecode -> Prop) -> Prop, (cache_inv_Property (snd decodePlusCacheInv) P_inv -> CorrectDecoder _ predicate predicate eq format (fst decodePlusCacheInv) (snd decodePlusCacheInv) format) /\ cache_inv_Property (snd decodePlusCacheInv) P_inv) /\ DecodeMEquivAlignedDecodeM (fst decodePlusCacheInv) decoder}.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.NArith.NArith Coq.Arith.Arith Coq.Numbers.Natural.Peano.NPeano Coq.Logic.Eqdep_dec Fiat.Narcissus.Common.Specs Fiat.Narcissus.BinLib.Core Fiat.Narcissus.BinLib.AlignedByteString