The Coq mailing list

[BruinBear123 AT aol.com]

Hi everyone.
How can you use Coq to show that...

(forall C: U0). C => (C => C) => C

can be seen as a representation of the type of natural numbers?


What I think this is saying is that the successor of a natural 
number is implied by a function that returns the successor and that in turn 
is implied by the argument that that function takes.
 
Is this a correct reading of the situation and how do you actually 'show' it?
Any help would be very much appreciated.
Many thanks,
Bill Brown.