proposition: Lemma Vmap_app : forall n1 n2 (v1 : vector A n1) (v2 : vector A n2), Vmap (Vapp v1 v2) = Vapp (Vmap v1) (Vmap v2).
proof: Proof. intros; induction v1. simpl; auto. simpl. rewrite IHv1. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)