proposition: Lemma select_lt : forall {A:Type} (l: list A) (a:A) n, select n l = Some a -> n < length l.
proof: Proof. introv Heq. assert (n<length l \/ n>=length l ) as XX by omega. dorn XX; auto. apply nth_select2 in XX. rewrite XX in Heq. inverts Heq. Qed.
imports: UsefulTypes bin_rels Omega