diff --git a/verification/verifast/proof/ready_list_predicates.h b/verification/verifast/proof/ready_list_predicates.h
index c06acf3b6..b3e4f3676 100644
--- a/verification/verifast/proof/ready_list_predicates.h
+++ b/verification/verifast/proof/ready_list_predicates.h
@@ -279,7 +279,7 @@ void VF_reordeReadyList(List_t* pxReadyList, ListItem_t * pxTaskItem)
             gPrefOwnerLists == take(gOffset, gOwnerLists) &*&
             gSufOwnerLists == drop(gOffset+1, gOwnerLists) &*&
             forall(gOwnerLists, (superset)(gTasks)) == true &*&
-            forall(gOwners, (mem_list_elem)(gTasks)) == true;
+            subset(gOwners, gTasks) == true;
 @*/
 /*@ ensures 
         readyLists_p(?gReorderedCellLists, ?gReorderedOwnerLists) &*&
@@ -291,6 +291,12 @@ void VF_reordeReadyList(List_t* pxReadyList, ListItem_t * pxTaskItem)
 {
     //@ open VF_reordeReadyList__ghost_args(_, _, _, _);
 
+    // Proving `∀o ∈ gOwners. o ∈ gTasks`
+        //@ forall_mem(gOwners, gOwnerLists, (superset)(gTasks));
+        //@ assert( superset(gTasks, gOwners) == true );
+        //@ subset_implies_forall_mem(gOwners, gTasks);
+    //@ assert( forall(gOwners, (mem_list_elem)(gTasks)) == true );
+
     // Proving `length(gCells) == length(gOwners) == gSize + 1`:
         //@ open xLIST(pxReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners);
         //@ close xLIST(pxReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners);