push the proof forward.  swapmCorrect is done, up to key-lemma, which is almost done and should be relatively straightforward to finish.