Slightly simplify proof of ucord_sup_exists_lemma.