include "basics/list.ma".

let rec nth_opt (A:Type[0]) (n:nat) (l:list A) on l : option A ≝
match l with
[ nil ⇒ None ?
| cons h t ⇒ match n with [ O ⇒ Some ? h | S m ⇒ nth_opt A m t ]
].

let rec All (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
match l with
[ nil ⇒ False
| cons h t ⇒ P h ∧ All A P t
].

let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool ≝
match l with
[ nil ⇒ false
| cons h t ⇒ orb (p h) (exists A p t)
].