proposition: Lemma select_in : forall {A:Type} (l: list A) (a:A) n, select n l = Some a -> LIn a l.
proof: Proof. introv Heq. duplicate Heq. apply select_lt in Heq. pose proof (nth_select1 _ _ a Heq) as XX. rewrite XX in Heq0. invertsn Heq0. pose proof (nth_in _ _ l a Heq) as XXX. auto. Qed.
imports: UsefulTypes bin_rels Omega