proposition: Lemma Vmap_map : forall A B C (f:A->B) (g:B->C) n (v : vector A n), Vmap g (Vmap f v) = Vmap (fun x : A => g (f x)) v.
proof: Proof. intros; induction v. simpl; refl. simpl Vmap at 2. simpl Vmap at 1. rewrite IHv. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)