proposition: Lemma constant_decode_correct {S V T} {cache : Cache} {P : CacheDecode -> Prop} {monoid : Monoid T} (view : S -> V -> Prop) (Source_Predicate : S -> Prop) (View_Predicate : V -> Prop) (format : FormatM V T) (view_format : FormatM V T) (decode_V : DecodeM (V * T) T) (const_v : V) (decode_V_OK : CorrectDecoder monoid View_Predicate View_Predicate eq format decode_V P view_format) (const_v_OK : View_Predicate const_v) : CorrectDecoder monoid Source_Predicate View_Predicate (fun _ v' => const_v = v') (Projection_Format format (constant const_v)) decode_V P view_format.
proof: Proof. eapply projection_decode_correct; eauto. Qed.
imports: Coq.ZArith.ZArith Coq.Strings.String Coq.Vectors.Vector Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.Narcissus.Common.Specs