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