New syntax for types allowing for tuples (proved sound).

The elaborator needs to be changed to map the string "" to the TC_tup
type identifier. I haven't done this because I couldn't figure out how
to invoke lem in the semantics directory.
Completeness now wrt 2 cheats.

Both are left-recursions that I think are quite doable.