proposition: Lemma finite_of_list_nodup l : nodup l -> finite (of_list l).
proof: Proof. destruct l. intros _. exists 0. exists any_of_N0. split. intros [x_val x]. intros; lia. intros [y_val y]. contradiction. rename l into l'. set (l := a :: l'). intro hl. set (n := length l). ex n. assert (i : forall k : N n, k < n). intros [k_val k]. simpl. lia. set (f := fun k : N n => elt (P:=of_list l) (nth_In a (i k))). ex f. split. intros [x_val x] [y_val y]. unfold f; simpl. intro e. apply N_eq; simpl. apply sig_eq in e; simpl in e. subst n. eapply inj_nth_nodup. 2: apply hl. apply eq_dec. hyp. hyp. apply e. intros [y_val y]. gen (In_nth a y); intros [k [k1 k2]]. ex (N_ k1). apply sig_eq; simpl. auto. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil NatUtil FunUtil ListUtil ListNodup SetUtil BoundNat)