proposition: Lemma Vforall_nth : forall n (v : vector A n) i (ip : i < n), Vforall v -> P (Vnth v ip).
proof: Proof. intros. apply Vforall_in with n v. hyp. apply Vnth_in. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)