proposition: Lemma Decode_w_Measure_lt_eq' : forall (A B : Type) (cache : Cache) (monoid : Monoid B) (A_decode : B -> CacheDecode -> option (A * B * CacheDecode)) (b : B) (cd : CacheDecode) (A_decode_lt : forall (b0 : B) (cd0 : CacheDecode) (a : A) (b' : B) (cd' : CacheDecode), A_decode b0 cd0 = Some (a, b', cd') -> lt_B b' b0) (a' : A) (b' : B) (cd' : CacheDecode) pf, Decode_w_Measure_lt A_decode b cd A_decode_lt = Some (a', pf, cd') -> A_decode b cd = Some (a', `pf , cd').
proof: Proof. unfold Decode_w_Measure_lt; intros. revert pf H. generalize (A_decode_lt b cd). destruct (A_decode b cd) as [ [ [? ?] ?] | ]; simpl; intros; try discriminate. injections; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.Strings.Ascii Coq.Strings.String Coq.Logic.Eqdep_dec Fiat.Computation.Core Fiat.Computation.FixComp Fiat.Computation.Notations Fiat.Computation.Refinements.General Fiat.Common.DecideableEnsembles Fiat.Narcissus.Common.Specs Fiat.Narcissus.Formats.FixStringOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.AsciiOpt