diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 4b534ce0718fc0c914ae4e285f0eea9671297274..9c6a17d6315924bd16b3c9fbec28dc841ec0fecc 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -320,6 +320,33 @@ Qed.
 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 elim_modal_embed_bupd_goal `{BUpdFacts PROP} P P' ð“  ð“ ' :
+  ElimModal P P' (|==> âŽ¡ð“ âŽ¤)%I (|==> âŽ¡ð“ 'âŽ¤)%I â†’
+  ElimModal P P' âŽ¡|==> ð“ âŽ¤ âŽ¡|==> ð“ 'âŽ¤.
+Proof. by rewrite /ElimModal !monPred_bupd_embed. Qed.
+Global Instance elim_modal_embed_bupd_hyp `{BUpdFacts PROP} ð“Ÿ P' Q Q' :
+  ElimModal (|==> âŽ¡ð“ŸâŽ¤)%I P' Q Q' â†’
+  ElimModal âŽ¡|==> ð“ŸâŽ¤ P' Q Q'.
+Proof. by rewrite /ElimModal monPred_bupd_embed. Qed.
+
+Global Instance add_modal_embed_bupd_goal `{BUpdFacts PROP} P P' ð“  :
+  AddModal P P' (|==> âŽ¡ð“ âŽ¤)%I â†’ AddModal P P' âŽ¡|==> ð“ âŽ¤.
+Proof. by rewrite /AddModal !monPred_bupd_embed. Qed.
+
+Global Instance elim_modal_at_bupd_goal `{BUpdFacts PROP} ð“Ÿ ð“Ÿ' Q Q' i :
+  ElimModal ð“Ÿ ð“Ÿ' (|==> Q i) (|==> Q' i) â†’
+  ElimModal ð“Ÿ ð“Ÿ' ((|==> Q) i) ((|==> Q') i).
+Proof. by rewrite /ElimModal !monPred_bupd_at. Qed.
+Global Instance elim_modal_at_bupd_hyp `{BUpdFacts PROP} P ð“Ÿ' ð“  ð“ ' i:
+  ElimModal (|==> P i) ð“Ÿ' ð“  ð“ ' â†’
+  ElimModal ((|==> P) i) ð“Ÿ' ð“  ð“ '.
+Proof. by rewrite /ElimModal monPred_bupd_at. Qed.
+
+Global Instance add_modal_at_bupd_goal `{BUpdFacts PROP} ð“Ÿ ð“Ÿ' Q i :
+  AddModal ð“Ÿ ð“Ÿ' (|==> Q i)%I â†’ AddModal ð“Ÿ ð“Ÿ' ((|==> Q) i).
+Proof. by rewrite /AddModal !monPred_bupd_at. Qed.
+
 End bi.
 
 (* When P and/or Q are evars when doing typeclass search on [IntoWand
@@ -384,4 +411,30 @@ Qed.
 Global Instance from_later_monPred_at i n P Q ð“  :
   FromLaterN n P Q â†’ MakeMonPredAt i Q ð“  â†’ FromLaterN n (P i) ð“ .
 Proof. rewrite /FromLaterN /MakeMonPredAt=> <- <-. elim n=>//= ? ->. by unseal. Qed.
+
+Global Instance elim_modal_embed_fupd_goal `{FUpdFacts PROP} E1 E2 E3 P P' ð“  ð“ ' :
+  ElimModal P P' (|={E1,E3}=> âŽ¡ð“ âŽ¤)%I (|={E2,E3}=> âŽ¡ð“ 'âŽ¤)%I â†’
+  ElimModal P P' âŽ¡|={E1,E3}=> ð“ âŽ¤ âŽ¡|={E2,E3}=> ð“ 'âŽ¤.
+Proof. by rewrite /ElimModal !monPred_fupd_embed. Qed.
+Global Instance elim_modal_embed_fupd_hyp `{FUpdFacts PROP} E1 E2 ð“Ÿ P' Q Q' :
+  ElimModal (|={E1,E2}=> âŽ¡ð“ŸâŽ¤)%I P' Q Q' â†’
+  ElimModal âŽ¡|={E1,E2}=> ð“ŸâŽ¤ P' Q Q'.
+Proof. by rewrite /ElimModal monPred_fupd_embed. Qed.
+
+Global Instance add_modal_embed_fupd_goal `{FUpdFacts PROP} E1 E2 P P' ð“  :
+  AddModal P P' (|={E1,E2}=> âŽ¡ð“ âŽ¤)%I â†’ AddModal P P' âŽ¡|={E1,E2}=> ð“ âŽ¤.
+Proof. by rewrite /AddModal !monPred_fupd_embed. Qed.
+
+Global Instance elim_modal_at_fupd_goal `{FUpdFacts PROP} E1 E2 E3 ð“Ÿ ð“Ÿ' Q Q' i :
+  ElimModal ð“Ÿ ð“Ÿ' (|={E1,E3}=> Q i) (|={E2,E3}=> Q' i) â†’
+  ElimModal ð“Ÿ ð“Ÿ' ((|={E1,E3}=> Q) i) ((|={E2,E3}=> Q') i).
+Proof. by rewrite /ElimModal !monPred_fupd_at. Qed.
+Global Instance elim_modal_at_fupd_hyp `{FUpdFacts PROP} E1 E2 P ð“Ÿ' ð“  ð“ ' i :
+  ElimModal (|={E1,E2}=> P i) ð“Ÿ' ð“  ð“ ' â†’
+  ElimModal ((|={E1,E2}=> P) i) ð“Ÿ' ð“  ð“ '.
+Proof. by rewrite /ElimModal monPred_fupd_at. 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_fupd_at. Qed.
 End sbi.