gwillen can occupy an actual room instead of sleeping on the futon.Fixed a bug where not even the simple types of terms were agreeing in HLF type inference; now it's down to fiddly deBruijn problems. It's extremely irritating that I have one view of the system which has only world variables, and another view from which I have term and world variables interleaved, and I keep mixing them up.