work towards proving new_specification_correct

reduced to a cheat that looks to be just about the semantics of
substitution: probably worth proving INST correct first then re-using
the appropriate lemma.