lemma setsum_diff_union
using shorter syntax
some steps towards "value_rel b x' ≥ value_rel b y'" deep inside wd_outcome proof