Round-six lemma `swIUP_spec`