proposition: Lemma decode_word_le : forall (b1 : T) (cd : CacheDecode) (a : word sz) (b' : T) (cd' : CacheDecode), decode_word b1 cd = Some (a, b', cd') -> le_B b' b1.
proof: Proof. unfold decode_word. intros; destruct (decode_word' sz b1) as [ [? ?] | ] eqn: ? ; subst; simpl in *; try discriminate. injections. eapply decode_word'_le; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Common Fiat.Computation.Notations Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.BaseFormats