proposition: Lemma ForallV_vector_In : forall {n} t (vs : vector T n) P, ForallV P vs -> vector_In t vs -> P t.
proof: Proof. induction 2. - eapply (ForallV_vector_hd H). - eapply IHvector_In. eapply (ForallV_vector_tl H). Qed.
imports: ExtLib.Data.Fin