diff --git a/algebra/upred.v b/algebra/upred.v
index 5083b9d753ec08d70ca2c794f7115acf3ae99b21..d41a5adecc01b1ef0486bc7c9441759675cfe64d 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -1513,6 +1513,9 @@ Section cmra.
     eapply uPred_mono with x1; eauto using cmra_includedN_l.
   Qed.
 
+  Lemma uPred_included P Q : P ≼ Q → Q ⊢ P.
+  Proof. intros [P' ->]. apply uPred.sep_elim_l. Qed.
+
   Definition uPred_cmra_mixin : CMRAMixin (uPred M).
   Proof.
     apply cmra_total_mixin; try apply _ || by eauto.