diff --git a/README b/README
index 53ccfc1bb8d08577edb61b5243af406f8a5acae1..3a3dd3dcd71ad25e0b6e9a93cfe0abaeb6d5cb0c 100644
--- a/README
+++ b/README
@@ -4,15 +4,9 @@ PREREQUISITES
 This version is known to compile with:
 
  - Coq 8.5
- - Ssreflect 1.6
+ - Ssreflect >= 3cc0493
  - Autosubst 1.4
 
-For development, better make sure you have a version of Ssreflect that includes
-commit be724937 (no such version has been released so far, you will have to
-fetch the development branch yourself). Iris compiles fine even without this
-patch, but proof bullets will only be in 'strict' (enforcing) mode with the
-fixed version of Ssreflect.
- 
 BUILDING INSTRUCTIONS
 ---------------------
 
diff --git a/barrier/lifting.v b/barrier/lifting.v
index 28a535e4dffa2ac2591a46f2e40f6b00b359e065..a2bd229f72627f67e4aac93a04e1ea0fcb08e783 100644
--- a/barrier/lifting.v
+++ b/barrier/lifting.v
@@ -21,10 +21,8 @@ Lemma wp_alloc_pst E σ e v Q :
   (ownP σ ★ ▷ (∀ l, ■(σ !! l = None) ∧ ownP (<[l:=v]>σ) -★ Q (LocV l)))
        ⊑ wp E (Alloc e) Q.
 Proof.
-  (* TODO RJ: Without the set, ssreflect rewrite doesn't work. Figure out why or
-     reprot a bug. *)
-  intros. set (φ v' σ' ef := ∃ l, ef = @None expr ∧ v' = LocV l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None).
-  rewrite -(wp_lift_atomic_step (Alloc e) φ σ) // /φ;
+  intros; rewrite -(wp_lift_atomic_step (Alloc e) (λ v' σ' ef,
+    ∃ l, ef = None ∧ v' = LocV l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None) σ) //;
     last by intros; inv_step; eauto 8.
   apply sep_mono, later_mono; first done.
   apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef.