new lemma disj_Un_runiq, simplified some further lemmas that depend on runiq