On the list 1::2:: ... n::nil
Build a function computing the list
1::2:: ... n::nil for every n of type
nat.
Solution
Look at this file
Note
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).