Taking ∃ out of ▷ without Inhabited, more easily
In Iris Proof Mode, destruction of ▷ (∃ (x: A), Φ a)
into (x) "H"
(where "H"
will assert ▷ Φ x
) always requires Inhabited A
, because it uses the lemma later_exist
.
In some situations, Inhabited A
is not known a priori.
If we use the lemma later_exist_except_0
instead, we get ▷ Φ x
without having Inhabited A
, under the ◇
modality.
In Iris we are often under the ◇
modality because the update modality |=>
contains ◇
.
I hope the operation of taking ∃x
out of ▷
without Inhabited
becomes easier to use.
One possibility is to let Iris Proof Mode apply later_exist_except_0
when the goal is under the ◇
modality.