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