proposition: Lemma Decode_w_Measure_lt_eq (b : T) (cd : CacheDecode) (S_decode_lt : forall (b : T) (cd : CacheDecode) (a : S) (b' : T) (cd' : CacheDecode), S_decode b cd = Some (a, b', cd') -> lt_B b' b) : forall a' b' cd', S_decode b cd = Some (a', b', cd') -> exists pf, Decode_w_Measure_lt b cd S_decode_lt = Some (a', exist _ b' pf , cd').
proof: Proof. clear; intros; unfold Decode_w_Measure_lt. remember (S_decode_lt b cd); clear Heql. destruct (S_decode b cd) as [ [ [? ?] ? ] | ]. injections; eauto. 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