proposition: Lemma Vmap_id : forall (A : Type) n (v : vector A n), Vmap (fun x => x) v = v.
proof: Proof. induction v. refl. simpl. apply Vcons_eq_intro; auto. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)