lemma Union_map_compr_eq1
wd_outcome: further payment well-definedness