fact: Fixpoint nth' (A:Set)(l:list A)(n:nat){struct n} : option A := match l, n with | nil, _ => None | cons a tl, O => Some a | cons a tl, S p => nth' A tl p end.
imports: ZArith List Arith Lia Zwf Inverse_Image Extraction