proposition: Lemma Vmap_tail : forall n (v : vector A (S n)), Vmap (Vtail v) = Vtail (Vmap v).
proof: Proof. intros. VSntac v. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)