renamed variable more intuitively
one more step in wd_outcome payment well-definedness
factored out generally usable ex1_imp_trivial and elem_in_uniq_eq_class