proposition: Lemma forall_Vector_P {A} (P : A -> Prop) {n} : forall v : Vector.t A n, Vector.Forall P v -> forall idx, P (Vector.nth v idx).
proof: Proof. induction v; simpl; intros. - inversion idx. - revert v IHv H; pattern n, idx; apply Fin.caseS; simpl; intros; inversion H; subst; eauto. eapply IHv. apply Eqdep_dec.inj_pair2_eq_dec in H2; subst; eauto using Peano_dec.eq_nat_dec. Qed.
imports: Fiat.Common.BoundedLookup Fiat.Narcissus.Common.Specs Fiat.Narcissus.BaseFormats Fiat.Narcissus.Formats.WordOpt Coq.Vectors.Vector Bedrock.Word