proposition: Lemma nth_select1: forall {A:Type} (n:nat) (l:list A) (def: A), n < length l -> select n l= Some (nth n l def).
proof: Proof. induction n as [|n Hind]; introv Hl; destruct l;try (inverts Hl;fail); simpl; auto. allsimpl. erewrite Hind; eauto. omega. Qed.
imports: UsefulTypes bin_rels Omega