split lemma-union-not-used into lemma-exchange-maps