fact: Fixpoint select {A:Type} (n:nat) (l:list A): option A := match n with | 0 => match l with | [] => None | x :: _ => Some x end | S m => match l with | [] => None | _ :: t => select m t end end.
imports: UsefulTypes bin_rels Omega