Unsound instantiation of existentials by `iFrame` on persistent facts
@janno and I found that the new support for existential instantiation in iFrame
(from !1017 (merged)) can sometimes instantiate existential quantifiers too eagerly for persistent facts.
Reproducing example:
Require Import iris.bi.interface.
Require Import iris.proofmode.proofmode.
Goal ∀ (PROP : bi) (P : nat -> PROP),
□ P 0 ⊢ P 0 ∗ (∀ n : nat, P n -∗ ∃ n, P n ∗ ⌜n = 1⌝).
Proof.
iIntros (??) "#$".
(*
PROP : bi
P : nat → PROP
============================
_ : P 0
--------------------------------------□
∀ x : nat, P x -∗ ⌜0 = 1⌝
*)
Abort.