proposition: Lemma Vmap_eq : forall (A B : Type) (f g : A->B) n (v : vector A n), Vforall (fun a => f a = g a) v -> Vmap f v = Vmap g v.
proof: Proof. induction v; simpl; intros. refl. destruct H. apply Vcons_eq_intro; auto. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)