fact: Fixpoint vec_of_val (n : nat) : vector I n := match n as n return vector _ n with | O => Vnil | S n' => Vadd (vec_of_val n') (xint n') end.
imports: Coq(List) CoLoR(LogicUtil NaryFunction VecUtil VecMax NatUtil)