Provide support for `is_Some None` in the tactics `done` and `naive_solver`.

Since option is used a lot, I think it's reasonable to provide special support for deriving contradictions from is_Some None in done and naive_solver.

It would be nicer if this support was less ad-hoc, but well...

This closes #221 (closed) and #180 (closed).