[TYPES] [Coq-Club] Gentzen proof and Kantor ordering

[Freek Wiedijk]

Hello,

The ordinals up to epsilon zero are one of the fundamental
notions in the ACL2 system.  See for instance:

<http://www.ccs.neu.edu/home/pete/pub/acl2-ordinal-arithmetic-acl2.pdf>

Note that in the ACL2 representation of ordinals there is
no limit constructor, it's all about powers of omega (the
"finite rooted trees" that Vladimir was talking about).

Freek