proposition: Lemma word_indexed_correct': forall n (v : Fin.t n) (w : word sz) (t : t (word sz) n), word_indexed w t = Some v -> w = nth t v.
proof: Proof. clear. induction v. - intros w tb; pattern n, tb; eapply Vector.caseS; simpl. intros; destruct (weqb w h) eqn: ?. eapply weqb_true_iff; eauto. destruct ( word_indexed w t); try discriminate. - intros w tb. revert w v IHv. pattern n, tb; eapply Vector.rectS; simpl; intros. inversion v. intros; destruct (weqb w a) eqn: ?. discriminate. destruct (word_indexed w v) eqn : ? ; try discriminate. eapply IHv. rewrite Heqo. f_equal. eapply Fin.FS_inj. congruence. Qed.
imports: Fiat.Common.BoundedLookup Fiat.Narcissus.Common.Specs Fiat.Narcissus.BaseFormats Fiat.Narcissus.Formats.WordOpt Coq.Vectors.Vector Bedrock.Word