proposition: Lemma no_repeats_index_unique: forall {T:Type} (a:T) (n1 n2:nat) (l:list T), no_repeats l -> select n1 l = Some a -> select n2 l = Some a -> n1 = n2.
proof: Proof. induction n1 as [| n1 Hind]; introv Hnr H1s H2s; auto; destruct l as [| h l]. inverts H1s. allsimpl. inverts Hnr. destruct n2; auto. allsimpl. invertsn H1s. apply select_in in H2s. sp. destruct n2; inverts H2s. allsimpl. destruct n2. inverts H2s. inverts Hnr. apply select_in in H1s. sp. f_equal. allsimpl. apply Hind with (l:=l); eauto. inverts Hnr; auto. Qed.
imports: UsefulTypes bin_rels Omega