proposition: Lemma Decode_w_Measure_le_eq'': forall (b : T) (cd : CacheDecode) (S_decode_le : forall (b0 : T) (cd0 : CacheDecode) (a : S) (b' : T) (cd' : CacheDecode), S_decode b0 cd0 = Some (a, b', cd') -> le_B b' b0), Decode_w_Measure_le b cd S_decode_le = None -> S_decode b cd = None.
proof: Proof. clear; intros ? ? ?; unfold Decode_w_Measure_le in *. remember (S_decode_le b cd); clear Heql. destruct (S_decode b cd) as [ [ [? ?] ? ] | ]; eauto. intros; 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