proposition: Lemma Vforall_nth_intro : forall n (v : vector A n), (forall i (ip : i < n), P (Vnth v ip)) -> Vforall v.
proof: Proof. intros. apply Vforall_intro. intros. destruct (Vin_nth H0) as [i [ip v_i]]. rewrite <- v_i. apply H. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)