[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Enumeration types

  I don't think you're doing anything wrong.
Logically, it doesn't make a difference whether you have
[1]   emptyT?(x)
[2]   zeroT?(x)

[-1]  succT?(x)

The simplifier treats them the same.  If you prefer the latter
form, I can see if there something I can do.  Please send me enough
information so that I can recreate your proof.