new inference rule lemma case_split_2_times_2
lemma Diff_replace: now using the assumptions that we (probably) actually need
syncing progress in first case of non-negative payments in wd_outcome