diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index b18cb809f590f073399ef6f2e52a443756765053..2c6fa9bb93e816044821ac8eda2c52b1ceee28d0 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -104,6 +104,15 @@ 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/class_instances.v b/theories/proofmode/class_instances.v
index 3268cc849ef1d7e729fcae8694ab37c6f1f6e3bf..9a0e3db9bd448503c3b7ab5f77ff94e2485f14e4 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -849,6 +849,10 @@ Global Instance from_forall_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A → PR
   FromForall P Φ → FromForall ⎡P⎤%I (λ a, ⎡Φ a⎤%I).
 Proof. by rewrite /FromForall -bi_embed_forall => <-. Qed.
 
+(* IntoInv *)
+Global Instance into_inv_embed {PROP' : bi} `{BiEmbed PROP PROP'} P N :
+  IntoInv P N → IntoInv ⎡P⎤ N.
+
 (* ElimModal *)
 Global Instance elim_modal_wand φ P P' Q Q' R :
   ElimModal φ P P' Q Q' → ElimModal φ P P' (R -∗ Q) (R -∗ Q').