proposition: Lemma Vforall_eq : forall n (v : vector A n), Vforall v <-> (forall x, Vin x v -> P x).
proof: Proof. split; intros. eapply Vforall_in. apply H. hyp. apply Vforall_intro. hyp. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)