# Make `iDestruct` work on `▷ ∃` if goal is except_0/update

BIs have the interesting rule `bi.later_exist_except_0`

which allows to commute `▷`

and `∃ x : A`

even if the domain `A`

of the existential is not inhabited:

`bi.later_exist_except_0 : ▷ (∃ a : A, Φ a) -∗ ◇ (∃ a : A, ▷ Φ a)`

Instead, you get an except-0 (`◇`

) modality, which can be eliminated if the goal is, for example, an update modality.

This trick is not commonly known, so it would be great if the proof mode's `iDestruct`

tactic could use `bi.later_exist_except_0`

automatically instead of just failing when the domain `A`

is not inhabited.

This is what happens now:

```
From iris.proofmode Require Import tactics.
From iris.bi Require Import updates.
Lemma test `{BiFUpd PROP} {A} (Φ : A → PROP) (Q : PROP) E :
▷ (∃ x, Φ x) ={E}=∗ Q.
Proof.
iIntros "H".
(* Goal:
"H" : ▷ (∃ x : A, Φ x)
--------------------------------------∗
|={E}=> Q *)
(* Tactic failure: iExistDestruct: cannot destruct (▷ (∃ x : A, Φ x))%I. *)
Fail iDestruct "H" as (x) "H".
(* Works *)
iMod (bi.later_exist_except_0 with "H") as (x) "H".
```

I tried to implement what I proposed in this MR some day, but I could not find a satisfactory generalization of the `IntoExist`

class. After all, that class then needs to take the goal into account to eliminate the ◇ modality.

An alternative, we could use the `pm_error`

infrastructure from #413 (which still needs to be ported to `IntoExists`

) to give an error that points the user to `bi.later_exist_except_0`

in case the domain `A`

is not inhabited.