fact: Definition Vmap_first n (v : vector A n) : B := match v with | Vcons a _ => f a | _ => default end.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)