push things forward a bit more (and simplify).  Need a lemma that says that subst is a congruence to finish this case.