Things going on today: meetings with Frank and
A historical point that I find interesting is that both the idea of separating inversion from pruning and the idea of inversion-failures showing up as free variables already occur in earlier work — in Tobias Nipkow's 1993 LICS paper, and Dowek-Hardin-Kirchner-Pfenning's JICSLP'96 paper, respectively. All that I've done that's new is proof things about their typing.
Also λs. I should write another real post about that.