Make `done` solve the goal when one of the Iris hypothesis is `False`
As in Coq, this should work even if the hypothesis is not syntacticaly False
, but only convertible to it.
As in Coq, this should work even if the hypothesis is not syntacticaly False
, but only convertible to it.