revert one of the last commits -- apparently s_run rule was correct. proof is stuck again.