diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 2c6fa9bb93e816044821ac8eda2c52b1ceee28d0..b18cb809f590f073399ef6f2e52a443756765053 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/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).
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index fd1e7e0568a2cd7d63cc629de29c9dee4584cbfa..cfec41ed65338ce0d56722274db1102e6f98b9f2 100644
--- a/theories/proofmode/monpred.v
+++ b/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.