proposition: Lemma ascii_decode_le : forall (b : B) (cd : CacheDecode) (a : ascii) (b' : B) (cd' : CacheDecode), decode_ascii b cd = Some (a, b', cd') -> le_B b' b.
proof: Proof. unfold decode_ascii, DecodeBindOpt2; intros. destruct (decode_word b cd) as [ [ [? ? ] ?] | ] eqn: decode_b; simpl in H; try discriminate; injections. eauto using decode_word_le. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.Narcissus.Common.Specs Fiat.Narcissus.BaseFormats Fiat.Narcissus.Formats.WordOpt Bedrock.Word Coq.ZArith.ZArith Coq.Strings.Ascii Coq.Numbers.BinNums Coq.NArith.BinNat