proposition: Lemma val_of_vec_eq : forall n (v : vector I n) x (h : x < n), val_of_vec v x = Vnth v h.
proof: Proof. intros. unfold val_of_vec. case (le_lt_dec n x); intro. absurd (x<n); lia. apply Vnth_eq. refl. Qed.
imports: Coq(List) CoLoR(LogicUtil NaryFunction VecUtil VecMax NatUtil)