swapmCorrect2 is the good way to prove this, should get put in place of the not-going-to-work swapmCorrect.  Needed more little lemmas on the way too.