I think I finally finished a proof I've been working on occasionally for the last couple weeks. It's not very long, but it's one of the trickiest induction hypotheses I've ever had to come up with. I think the only one that beats it is the crazy labelled deduction callcc nonsense I did some time ago. It's up on my drafts page as "terminating untyped hereditary substitution". For a quick summary: hereditary substitution works because, although it hereditarily carries out β-reductions, sometimes it throws its hands up and rejects the substitution currently being carried out. This is why it can terminate, even on ill-typed terms, and indeed it will always terminate if you rig it up with a type index. Now imagine doing things in spine form, but leave off the type index entirely. However, make sure that reduction of a lambda against an empty spine is rejected. It turns out substitution still terminates on all terms, be they well-typed or not! The proofs work by inferring some sort of quasi-typey things from the terms involved, and using them as the induction measure. I don't know what this result is good for, but it makes me happy to know the answer. At least assuming I didn't make a mistake somewhere... Also today was practice with n1h2k. We got through more songs than usual, I think, due to effective "let's just get through this list of songs that, seriously, we should all know by know" motivation.