fact: Definition Vid n : vector A n -> vector A n := match n with | O => fun _ => Vnil | _ => fun v => Vcons (Vhead v) (Vtail v) end.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)