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.
Similarly 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).