Require Export lists.
Section Some_nth.
Variable A : Type.
Variable P : A → Prop.
Definition some_nth(l : list A) : Prop :=
∃(n : nat)(n_less : n < length l), P (nth l n n_less).
Lemma some_nth_some :
∀(l : list A)(n : nat)(n_less : n < length l),
P (nth l n n_less) → some_nth l.
Lemma some_nth_singleton :
∀(a : A), P a ↔ some_nth [a].
End Some_nth.
Implicit Arguments some_nth [A].