add explicit roll/unroll for pedagogical purposes

[cyrus-]

We can do anonymous recursive types now:

There is no need for explicit roll or unroll, but for teaching isorecursive types it would be nice to have the option to include them.