On the list 1::2:: ... n::nil
Build a function computing the list
1::2:: ... n::nil for every n of type
Look at this file
This solution uses an anonymous recursive function (with fix).
If you want to prove some properties of the main function, it could be
useful to give a name to this auxiliary function (i.e to define
it with Fixpoint).