Round-six lemma `dIn_run`