proposition: Lemma Vin_vec_of_list : forall l x, In x l <-> Vin x (vec_of_list l).
proof: Proof. induction l; simpl; intros. tauto. rewrite (IHl x). tauto. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)