diff --git a/verification/verifast/proof/ready_list_predicates.h b/verification/verifast/proof/ready_list_predicates.h
index 549586ff1..c06acf3b6 100644
--- a/verification/verifast/proof/ready_list_predicates.h
+++ b/verification/verifast/proof/ready_list_predicates.h
@@ -285,7 +285,8 @@ void VF_reordeReadyList(List_t* pxReadyList, ListItem_t * pxTaskItem)
         readyLists_p(?gReorderedCellLists, ?gReorderedOwnerLists) &*&
         length(gReorderedCellLists) == length(gCellLists) &*&
         length(gReorderedOwnerLists) == length(gOwnerLists) &*&
-        length(gReorderedCellLists) == length(gReorderedOwnerLists);
+        length(gReorderedCellLists) == length(gReorderedOwnerLists) &*&
+        forall(gReorderedOwnerLists, (superset)(gTasks)) == true;
  @*/
 {
     //@ open VF_reordeReadyList__ghost_args(_, _, _, _);