[TYPES] Gentzen proof and Kantor ordering

[Thomas Streicher]

> If I recall correctly the ordinal numbers smaller than epsilon zero can be represented by finite rooted trees (non planar). It is then not difficult to describe constructively the ordinal partial ordering on them. Gentzen theorem says that if this partial ordering is well-founded then Peano arithmetic is consistent.
> 
> What can we prove about this ordering in Coq?

Already intuitionisti second order arithmetic does the job and thus so
does Coq.
Pure MLTT without universes wan't do it unless you have sufficient W-types.
But such a pure MLTT cannot even prove  not(0 = suc(x)). However,
adding a constant for that is possible and we'd arrive at a system of
the strength of HA whih can't recognize indutivity of epsilon_0.

thomas