proposition: Lemma N_eq {n} : forall x y : N n, N_val x = N_val y <-> x = y.
proof: Proof. intros [x xn] [y yn]; simpl. split; intro e. subst y. rewrite (lt_unique xn yn). refl. gen (f_equal N_val e). tauto. Qed.
imports: CoLoR(LogicUtil NatUtil ListUtil ListNodup FunUtil VecUtil)