diff --git a/barrier/barrier.v b/barrier/barrier.v
index 50569b44e6882e64ce1f71618389087c5b67c643..224c0e889da2ac20315cdf3df92397ede1b87ad9 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -203,8 +203,9 @@ Section proof.
     (* Now we come to the core of the proof: Updating from waiting to ress. *)
     rewrite /waiting /ress sep_exist_l. apply exist_elim=>{Q} Q.
     rewrite later_wand {1}(later_intro P) !assoc wand_elim_r.
-    (* TODO: Now we need stuff about Π★{set I} *)
-  Abort.
+    rewrite -big_sepS_later -big_sepS_sepS. apply big_sepS_mono'=>i.
+    rewrite -(exist_intro (Q i)) comm. done.
+  Qed.
 
   Lemma wait_spec l P (Q : val → iProp) :
     heapN ⊥ N → (recv l P ★ (P -★ Q '())) ⊑ wp ⊤ (wait (LocV l)) Q.