Awesome reply, thanks! Excuse me if more careful reading of your post would also answer these questions:
* What is the `M` in `h(UXT,IXT) → M[h(UXT,IXT)]`? How come `h` "arrows to" both `M[h(UXT,IXT)]` and `((XT,_),(XT,IT))`? A syntactic distinction between "is of type" and "this is its implementation" might help here, but I probably misread it. * What is `IXT`? You only defined `IT` and `UIT` afaict.
