Hereditary substitution with a universe hierarchy
As of November 2018, how to do this for dependent type theories with large eliminations is an open question. 

Establishing that the recursion is well-founded is not too bad; you can use Pataraia's theorem to prove the fixed point you want exists. See Robert Harper's *Constructing Type Systems Over an Operational Semantics for a how-to. (You can also do this via an inductive-recursive definition.)

The hard part is actually formulating the hereditary substitution in a nice way -- the natural direction leads you towards substituting not one term, but an entire substitution for a context, and this raises a lot of questions about when and how to establish properties of things like compositions of (hereditary) substitutions. 

If it turned out to be impossible, I would be utterly shocked. However, at present no one has done it. If you want to work on this, I would suggest getting in touch with Andreas Abel, Dan Licata and Mike Shulman. (Or me, for that matter.)