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
--------------------------------------□
?Pthen 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?