"done" should be able to make use of `is_Some None`

A goal of is_Some (Some _) is solved by done, but an assumption of is_Some None is not exploited by done. That feels weirdly asymmetric.

How hard would it be to fix that?