diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 3e6cbf6b5fd2e0050bebd41c2b0cc8b2ca48266a..e0ac53384630ad65ba099dc5741d08933422f9d3 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -413,6 +413,10 @@ Proof. unseal. rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim //. Qed
 Lemma monPred_impl_force P Q i : (P → Q) i -∗ (P i → Q i).
 Proof. unseal. rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim //. Qed.
 
+Lemma monPred_car_embed (P : PROP) (i : I) :
+  (bi_embed (B := monPred _ _) P) i ⊣⊢ P.
+Proof. by unseal. Qed.
+
 Lemma monPred_persistently_if_eq p P i:
   (bi_persistently_if p P) i = bi_persistently_if p (P i).
 Proof. rewrite /bi_persistently_if. unseal. by destruct p. Qed.