proposition: Lemma Vforall_in : forall x n (v : vector A n), Vforall v -> Vin x v -> P x.
proof: Proof. induction v; simpl. contr. intros Ha Hv. destruct Ha. destruct Hv. rewrite <- H1. exact H. auto. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)