As a final low-level LF thought for today: a while back I figured out to show that, if you define it right, (in particular in such a way that violations of η-longness like [λx.M/y]y are undefined) hereditary substitution terminates on all terms whether well-typed or not. The key thing is just showing that you can sort of infer adequate "types" for all terms, and use them as an induction measure. There's functions tp(M) and tp(S) that tell you roughly what type M is and what type of head the spine S expects, and a function (x ∈ M) that returns a set of types that x seems to have inside M. After showing that any substitution makes the type of the subject smaller, it's pretty straightforward to show that [M/x]N and [M|S] always terminate, by induction on something like tp(M) + (x ∈ N) in the first case, and tp(M) + tp(S) in the second, where "+" is a (commutative) formal sum.
So anyway today I think I figured out how to use the same ideas to show the standard commutativity property of substitution and reduction holds without any type labels or well-typedness assumptions. Specifically I can show (assuming y not in FV(M))
I) [M/x][N/y]P = [[M/x]N/y][M/x]P
II) [M/x][N|S] = [[M/x]N|[M/x]S]
if all the inner substitutions and reductions on both sides are well-defined. The induction measure is
I) tp(M) + tp(N) + (y ∈ P)
II) tp(M) + tp(N) + tp(S)
and the proof itself looks just like the usual one.