Define some flipped monotonicity Propers for binary uPred connectives.

No idea why these aren't resolved automatically, for unary predicates
they do not seem necesarry.

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).

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 :