proposition: Lemma Vin_map : forall x n (v : vector A n), Vin x (Vmap v) -> exists y, Vin y v /\ x = f y.
proof: Proof. induction v; simpl; intros. contr. destruct H. subst x. exists h. auto. assert (exists y, Vin y v /\ x = f y). apply IHv. hyp. destruct H0 as [y]. exists y. intuition. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)