  As part of the author's studies on equational reasoning for monadic programs,
this report focus on non-determinism monad.
  We discuss what properties this monad should satisfy, what additional
operators and notations can be introduced to facilitate equational reasoning
about non-determinism, and put them to the test by proving a number of
properties in our example problem inspired by the author's previous work on
proving properties of Spark aggregation.
