Frank poked a hole in something I was playing with not at all related to thesis whose fix (if correct) rendered the encoding a hojillion times more elegant. That is the best kind of bug to find.
---
Oh, wait, maybe it's still broken. Turns out regarding the sequent calculus version of Frank's labeled natural deduction for S4, it's not even clear what it is.
