Move export_rewrites of MAP and FLAT earlier in listScript.
List monad related definitions (mimicking what's in option)

Also adding the "apply" operator, which is the analogue of what on
options would be

  APPLY (SOME f) (SOME x) = SOME (f x)
  APPLY _ _ = NONE

Prove some relevant theorems.