proposition: Lemma projection_decode_correct {S V T} {cache : Cache} {P : CacheDecode -> Prop} {monoid : Monoid T} (project : S -> V) (Source_Predicate : S -> Prop) (View_Predicate : V -> Prop) (format : FormatM V T) (view_format : FormatM V T) (decode_V : DecodeM (V * T) T) (decode_V_OK : CorrectDecoder monoid View_Predicate View_Predicate eq format decode_V P view_format) (View_Predicate_OK : forall (s : S), Source_Predicate s -> View_Predicate (project s)) : CorrectDecoder monoid Source_Predicate View_Predicate (fun s v => project s = v) (Projection_Format format project) decode_V P view_format.
proof: Proof. eapply Compose_decode_correct; intros; eauto. subst; eauto. Qed.
imports: Coq.ZArith.ZArith Coq.Strings.String Coq.Vectors.Vector Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.Narcissus.Common.Specs