Support framing pure/Coq hypotheses
In the following, iFrame does not have the expected behavior:
Lemma L `{irisG Λ Σ} : ∀ P:iProp Σ, □ P ⊢ P ★ True. iIntros (P) "#HP". iFrame.
In the following, iFrame does not have the expected behavior:
Lemma L `{irisG Λ Σ} : ∀ P:iProp Σ, □ P ⊢ P ★ True. iIntros (P) "#HP". iFrame.