iDestruct does not handle some patterns that it probably could
The pattern match in
iDestructHypGo misses a handful of patterns that perhaps it could process. For example
IDone could probably be given a sensible interpretation.
iDestructHypFindPat complains about
H // even though that could be processed as
iDestruct ... as H; done. It does handle
H /= (by running
simpl after the destruct).