fact: Definition CorrectEncoder (format : FormatM) (encode : EncodeM) := (forall (a : S) (env : CacheFormat) (b : T) (xenv : CacheFormat), encode a env = Some (b, xenv) -> format a env ∋ (b, xenv)) /\ (forall (a : S) (env : CacheFormat), encode a env = None -> forall b xenv, ~ (format a env ∋ (b, xenv))).
imports: Coq.Lists.List Fiat.Common Fiat.Computation.Core Fiat.Computation.Notations Fiat.Narcissus.Common.Notations Fiat.Narcissus.Common.Monoid Fiat.Narcissus.Stores.Cache