proposition: Lemma no_repeats_index_unique2: forall {T:Type} (l:list T) (a:T) (n1 n2:nat) (def1 def2: T), no_repeats l -> n1 < length l -> n2 < length l -> (nth n1 l def1 =a) -> (nth n2 l def2 =a) -> n1 = n2.
proof: Proof. introv K1 K2 K3 K4 K5. apply nth_select3 in K4; auto. apply nth_select3 in K5; auto. pose proof (no_repeats_index_unique _ _ _ _ K1 K4 K5). trivial. Qed.
imports: UsefulTypes bin_rels Omega