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.