Draft: Make sure -#H pattern uses intuitionistic trick
This makes iDestruct (foo with "H") as "-#H2"
attempt to keep H
by showing the conclusion of foo
is persistent.
There are a couple problems with this:
-
iDestruct "H" as "-#H"
works even ifH
isn't persistent. This is inconsistent with the above. We could make it consistent with some more implementation. - (really minor incompatibility) you can no longer do
iDestruct (foo with "H") as "-#H2"
if the conclusion isn't persistent. Why you would have ever done this is beyond me.