proposition: Lemma Vin_V_elim n x : Vin x (V n) -> exists i, N_val x = n - i.
proof: Proof. destruct n; simpl. fo. intro xl. destruct (Vin_V_aux_elim xl) as [i e]. ex (S i). hyp. Qed.
imports: CoLoR(LogicUtil NatUtil ListUtil ListNodup FunUtil VecUtil)