Replace elim_inv_embed_inv by the more generic instance elim_inv_embed.

theories/base_logic/lib/invariants.v

@@ -104,15 +104,6 @@ Proof.
   iApply (Helim with "[$H2]"); first done.
   iMod (inv_open _ N with "[#]") as "(HP&Hclose)"; auto with iFrame.
 Qed.
-Global Instance elim_inv_embed_inv {PROP' : sbi} `{SbiEmbedding _ PROP'}
-       E N (P : iProp Σ) (Q Q' : PROP') :
-  (∀ R, ElimModal True ⎡|={E,E∖↑N}=> R⎤ ⎡R⎤ Q Q') →
-  ElimInv (↑N ⊆ E) ⎡inv N P⎤ True (⎡▷ P⎤) (⎡▷ P ={E∖↑N,E}=∗ True⎤) Q Q'.
-Proof.
-  rewrite /ElimInv /ElimModal. iIntros (Helim ?) "(#H1&TRUE&H2)".
-  rewrite -bi_embed_sep. iApply (Helim with "[$H2 $TRUE]"); first done.
-  iModIntro. iMod (inv_open _ N with "[#]") as "(HP&Hclose)"; auto with iFrame.
-Qed.
 
 Lemma inv_open_timeless E N P `{!Timeless P} :
   ↑N ⊆ E → inv N P ={E,E∖↑N}=∗ P ∗ (P ={E∖↑N,E}=∗ True).

theories/proofmode/monpred.v

@@ -490,4 +490,13 @@ Proof. by rewrite /ElimModal monPred_at_fupd. Qed.
 Global Instance add_modal_at_fupd_goal `{FUpdFacts PROP} E1 E2 𝓟 𝓟' Q i :
   AddModal 𝓟 𝓟' (|={E1,E2}=> Q i) → AddModal 𝓟 𝓟' ((|={E1,E2}=> Q) i).
 Proof. by rewrite /AddModal !monPred_at_fupd. Qed.
+
+Global Instance elim_inv_embed φ 𝓟inv 𝓟in 𝓟out 𝓟close Pin Pout Pclose Q Q' :
+  (∀ i, ElimInv φ 𝓟inv 𝓟in 𝓟out 𝓟close (Q i) (Q' i)) →
+  MakeEmbed 𝓟in Pin → MakeEmbed 𝓟out Pout → MakeEmbed 𝓟close Pclose →
+  ElimInv φ ⎡𝓟inv⎤ Pin Pout Pclose Q Q'.
+Proof.
+  rewrite /MakeEmbed /ElimInv=>H <- <- <- ?. iStartProof PROP.
+  iIntros (?) "(?&?&HQ')". iApply H; [done|]. iFrame. iIntros "?". by iApply "HQ'".
+Qed.
 End sbi.