Type alias 3

[dedbox]

Continuing the good work started in #505 .

This PR migrates the positive changes from PR #505 while eliding spurious edits and undesirable extensions to internal APIs, such as persistent modification of elaboration contexts in the statics.

[dedbox]

I've also been keeping this branch up to date with #558 for code exploration and some unit testing.

[dedbox]

edit action history panel is still seeing bug where spacing is screwed up due width of "tvar" badge when constructing a tpat

I can't reproduce this in latest chrome or firefox. Maybe you used a different browser?

[cyrus-]

This is Firefox on Linux. Notice misaligned arrows on right.

[cyrus-]

Archiving this. We are exploring some new approaches that are less finicky than de Bruijn indices now, but this might be a useful reference in any case -- see #612.