fact: Fixpoint val_of_vec2 n (v : vector I n) : valuation := fun x => match x, v with | _, Vnil => some_elt I | 0, Vcons a _ => a | S x', Vcons _ v' => val_of_vec2 v' x' end.
imports: Coq(List) CoLoR(LogicUtil NaryFunction VecUtil VecMax NatUtil)