proposition: Lemma Vforall_intro : forall n (v : vector A n), (forall x, Vin x v -> P x) -> Vforall v.
proof: Proof. induction v; simpl; intros. exact I. split. apply H. left. refl. apply IHv. intros. apply H. right. hyp. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)