Woke up, and worked out, at last, I think, how to do the translation from LF to LF*. At first I thought that I'd have to actually define a function whose domain was typing derivations, yecch. I hate trying to work out the syntax of that, involving huge \left(s and \right)s around prooftree environments. Fortunately, I think I know how to avoid that now, though my first attempt got pretty far before I realized I needed more type information around, and that doomed that.
Man, dependent type theories are like rampantly incestual families, I tell you. Terms gettin' with types, types gettin' with terms... A fella cain't hardly sort it all out.