The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

You can either define a function that indexes a list and takes a proof  
that the index is strictly smaller than the length of the list and use  
that function instead of 'nth', or else use vectors instead (which are  
lists of a particular length).

Edsko