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].