Make `done` work on `is_Some`.

Merged Robbert Krebbers requested to merge robbert/done_is_Some into master

Merge request reports