minor formatting
naming conventions as in Finite_Set
commented inconsistent definition
new lemmas Union_map_member, Union_map_non_empty
simplified a step in injections_exist
got paper-style arg max right
got paper-style arg max right, a bit more progress in wd_outcome