proposition: Lemma nth_error_ok_in : forall (A : Set) n (l : list A) (a : A), nth_error l n = Some a -> In a l.
proof: Proof. intros A n l; generalize n; clear n; induction l as [ | a' l]. intros [ | n] a; simpl; discriminate. intros [ | n] a; simpl. intro H; injection H; subst; left; trivial. intro; right; apply IHl with n; trivial. Qed.
imports: List Arith