proposition: Lemma CorrectDecoderNone (monoid : Monoid T) {V} : forall (Source_Predicate : S -> Prop) (View_Predicate : V -> Prop) (format : FormatM) (decode : _) (view : S -> V -> Prop) (decode_inv : CacheDecode -> Prop) (view_format : V -> CacheFormat -> Comp (T * CacheFormat)), CorrectDecoder _ Source_Predicate View_Predicate view format decode decode_inv view_format -> forall b b' s_d, decode_inv s_d -> decode (mappend b b') s_d = None -> forall a s_e s_e', Equiv s_e s_d -> Source_Predicate a -> format a s_e ∌ (b, s_e').
proof: Proof. unfold not, CorrectDecoder; intros. split_and. eapply H5 in H4; eauto. destruct_ex; split_and. rewrite H6 in H1; discriminate. Qed.
imports: Coq.Lists.List Fiat.Common Fiat.Computation.Core Fiat.Computation.Notations Fiat.Narcissus.Common.Notations Fiat.Narcissus.Common.Monoid Fiat.Narcissus.Stores.Cache