I had idea number eleventy billion and four about how to avoid huge explicit-context machinery and still get the job done of proving dependent hereditary substitution correct in twelf. It's becoming a bit of a windmillish theme in my life, but dang if I don't keep tilting at it.

The basic idea was pretty simple, actually. Modify the induction hypothesis, by creating a constant, call it "it", at the top-level, which ordinarily lacks any clause in the definition of typing to make it well-typed, to play the role of the variable being substituted for, and then defining a variant of the substitution function that knows to look for this special constant, and substitute for it. Naively this eliminates the usual immediate problems with inducting on a variable that appears in typing hypotheses. This means it looks you can pull the same sort of trick you do to get non-dependent hereditary substitution to work: just plug in "it", so that the main lemma to show is something like

thm: (hof it B -> of M A)
    -> of N B
    -> isub N M M'
    -> isub_tp N A A'
    -> of M' A'

Sadly, after banging my head on the wall for a few hours, I am still stuck in that limbo state of lacking any clear reason why some version of it shouldn't work, and yet also lacking any proof.