diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index df0833cd85c099aa20c89866f074b3fa6b45d452..aa15d3dd2754a6bca062610434aca5e9a68a95c2 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -354,6 +354,9 @@ Global Instance from_modal_monPred_at i P Q 𝓠 :
   FromModal P Q → MakeMonPredAt i Q 𝓠 → FromModal (P i) 𝓠.
 Proof. by rewrite /FromModal /MakeMonPredAt=> <- <-. Qed.
 *)
+Global Instance into_embed_absolute P :
+  Absolute P → IntoEmbed P (∀ i, P i).
+Proof. rewrite /IntoEmbed=> ?. by rewrite {1}(absolute_absolutely P). Qed.
 End bi.
 
 (* When P and/or Q are evars when doing typeclass search on [IntoWand
diff --git a/theories/tests/proofmode_monpred.v b/theories/tests/proofmode_monpred.v
index 7475fab4e5de0bfd7d88a597271d95e12f4afd51..70833d974ddd5e0f95993e00d97e1887a6d05caa 100644
--- a/theories/tests/proofmode_monpred.v
+++ b/theories/tests/proofmode_monpred.v
@@ -84,6 +84,10 @@ Section tests.
     □ P -∗ Q -∗ ⎡𝓟⎤ -∗ ⎡𝓠⎤ -∗ ⎡ 𝓟 ∗ 𝓠 ⎤.
   Proof. iIntros "#H1 _ H2 H3". iAlways. iFrame. Qed.
 
+  Lemma test_iModIntro_embed_absolute P `{!Absolute Q} 𝓟 𝓠 :
+    □ P -∗ Q -∗ ⎡𝓟⎤ -∗ ⎡𝓠⎤ -∗ ⎡ ∀ i, 𝓟 ∗ 𝓠 ∗ Q i ⎤.
+  Proof. iIntros "#H1 H2 H3 H4". iAlways. iFrame. Qed.
+
   (* This is a hack to avoid avoid coq bug #5735: sections variables
      ignore hint modes. So we assume the instances in a way that
      cannot be used by type class resolution, and then declare the