proposition: Lemma in_list_of_vec : forall n (v : vector A n) x, In x (list_of_vec v) -> Vin x v.
proof: Proof. induction v; simpl; intros. hyp. destruct H; auto. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)