fix s_run
complete an admitted case in proof of progress theorem