I am getting back some encouraging results for my hereditary substitution twelf idea. The main mutual induction goes through, and I've got it reduced to 5 lemmas that should go through without reference to the fact that substitution works, but the road to hell is paved with proof by really ought to be true.