proposition: Lemma nth_in : forall A n (l : list A) d, n < length l -> LIn (nth n l d) l.
proof: Proof. intros A n l d H; revert n H. induction l; simpl; sp. destruct n; sp. allapply S_lt_inj; sp. Qed.
imports: UsefulTypes bin_rels Omega