How to express a list of any type X?

Using Coq
1

Define function itemAtIndex that receives an index n
and a list of any type X, and returns the item in the
list in the given index n. Note that indexing starts
from 0.

2

Maybe like this?

Inductive List (T: Set): Set :=
| Link: T → List T → List T
| End: List T
.

Arguments Link {_} _.
Arguments End {_}.

Fixpoint itemAtIndex {T: Set} (index: nat) (xs: List T): option T :=
  match index, xs with
    | S index', Link _ xs' => itemAtIndex index' xs'
    | S _, End => None
    | Z, Link x _ => Some x
    | Z, End => None
  end.

So, you simply supply the type of the list’s elements as another argument. Since in Coq types are also terms, there is a unified way to deal with types and values — unlike in C, Haskell or OCaml, where expressions for types and for values can never be mixed. I made this argument implicit on the data constructors Link and End but it is entirely optional to do so.

3

Is nth or nth_error from the standard library, what you are looking for?