Swap now produces a correct post condition, although the tactics are
still not powerful enough to actually prove it.