diff --git a/logic/upred.v b/logic/upred.v
index 01f467cb0ee4c0e4abe110b5110a0f50cb376506..c8c4c26a6f76779b62235839b3259541db4f0170 100644
--- a/logic/upred.v
+++ b/logic/upred.v
@@ -486,8 +486,14 @@ Global Instance const_mono' : Proper (impl ==> (⊑)) (@uPred_const M).
 Proof. intros φ1 φ2; apply const_mono. Qed.
 Global Instance and_mono' : Proper ((⊑) ==> (⊑) ==> (⊑)) (@uPred_and M).
 Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
+Global Instance and_flip_mono' :
+  Proper (flip (⊑) ==> flip (⊑) ==> flip (⊑)) (@uPred_and M).
+Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
 Global Instance or_mono' : Proper ((⊑) ==> (⊑) ==> (⊑)) (@uPred_or M).
 Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
+Global Instance or_flip_mono' :
+  Proper (flip (⊑) ==> flip (⊑) ==> flip (⊑)) (@uPred_or M).
+Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
 Global Instance impl_mono' :
   Proper (flip (⊑) ==> (⊑) ==> (⊑)) (@uPred_impl M).
 Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
@@ -591,6 +597,9 @@ Proof. by intros x [|n] ?; [done|intros (x1&x2&?&?&[a ?]); exists a,x1,x2]. Qed.
 Hint Resolve sep_mono.
 Global Instance sep_mono' : Proper ((⊑) ==> (⊑) ==> (⊑)) (@uPred_sep M).
 Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
+Global Instance sep_flip_mono' :
+  Proper (flip (⊑) ==> flip (⊑) ==> flip (⊑)) (@uPred_sep M).
+Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
 Lemma wand_mono P P' Q Q' : Q ⊑ P → P' ⊑ Q' → (P -★ P') ⊑ (Q -★ Q').
 Proof. intros HP HQ; apply wand_intro_r; rewrite HP -HQ; apply wand_elim_l. Qed.
 Global Instance wand_mono' : Proper (flip (⊑) ==> (⊑) ==> (⊑)) (@uPred_wand M).
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index c028b22ce684f4742d6937cef16814571536178b..3618be406b3940a281b55d8d45bf4d30e591ee59 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -74,9 +74,7 @@ Proof.
   apply const_elim_l=>-[v2' [Hv ?]] /=.
   rewrite -pvs_intro.
   rewrite (forall_elim v2') (forall_elim σ2') (forall_elim ef) const_equiv //.
-  rewrite left_id wand_elim_r. apply sep_mono; last done.
-  (* FIXME RJ why can't I do this rewrite before doing sep_mono? *)
-  by rewrite -(wp_value' _ _ e2').
+  by rewrite left_id wand_elim_r -(wp_value' _ _ e2').
 Qed.
 
 Lemma wp_lift_atomic_det_step {E Q e1} σ1 v2 σ2 ef :