fact: Fixpoint V_aux k := match k as k return k<n -> vector (N n) (S k) with | 0 => fun h => Vcons (N_ h) Vnil | S k' => fun h => Vcons (N_ h) (V_aux k' (L_ h)) end.
imports: CoLoR(LogicUtil NatUtil ListUtil ListNodup FunUtil VecUtil)