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