proposition: Lemma ExtractViewFromRefined {S V T} : forall (cache : Cache) (monoid : Monoid T) (Source_Predicate : S -> Prop) (View_Predicate : V -> Prop) (view : S -> V -> Prop) (format : FormatM S T) (decode_inv : CacheDecode -> Prop) (v : V) (v_OK : View_Predicate v), (forall s', Source_Predicate s' -> view s' v) -> CorrectRefinedDecoder monoid Source_Predicate View_Predicate view format empty_Format (fun t' ctxD => Some (v, t', ctxD)) decode_inv empty_Format.
proof: Proof. intros; eapply ExtractViewFrom; eauto. intros; apply unfold_computes; intros. intuition. unfold empty_Format; apply unfold_computes; eauto. Qed.
imports: Coq.ZArith.ZArith Fiat.Common Fiat.Computation.Notations Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Computation.Refinements.General Fiat.Narcissus.BaseFormats