proposition: Lemma N_eq_dec {n} : forall x y : N n, {x=y}+{~x=y}.
proof: Proof. intros [x xn] [y yn]. destruct (eq_nat_dec x y). left. apply N_eq. hyp. right. intro e. apply n0. apply N_eq in e. hyp. Defined.
imports: CoLoR(LogicUtil NatUtil ListUtil ListNodup FunUtil VecUtil)