lemma arg_max'_non_empty_iff
factored tie breakers out into a separate theory
fixed a bug due to refactoring
further progress in wd_outcome