fact: Definition val_of_vec n (v : vector I n) : valuation := fun x => match le_lt_dec n x with | left _ => some_elt I | right h => Vnth v h end.
imports: Coq(List) CoLoR(LogicUtil NaryFunction VecUtil VecMax NatUtil)