proposition: Lemma in_nth: forall e (l : list A), In e l -> forall d, exists n, nth n l d = e /\ (n < length l)%nat.
proof: Proof. induction l; intros. inversion H. simpl in H. destruct H. subst. exists O. simpl. auto with arith. elim IHl with d. intros. exists (S x). simpl. intuition auto with arith. trivial. Qed.
imports: Coq(List) Coq(Arith)