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.