done when goal is evar picks unnecessarily strong
When the goal is an evar (and that evar does not appear otherwise in the current goal), like in
_ : inv nroot (∃ x' : Z, l ↦ #x')%I
--------------------------------------□
?P
then doing done
will pick a persistent (or spatial, I guess) hypothesis instead of just True
or emp
.
Maybe we should add bi.True_intro
with high priority to the database?