diff --git a/tasks.c b/tasks.c
index c31607902..3a35acd28 100644
--- a/tasks.c
+++ b/tasks.c
@@ -1033,10 +1033,15 @@ static void prvYieldForTask( TCB_t * pxTCB,
                  * must not be decremented any further */
                 xDecrementTopPriority = pdFALSE;
                 
+                //@ mem_nth(uxCurrentPriority, gCellLists);
+                //@ assert( mem(gCells, gCellLists) == true);
+                //@ open_collection_of_sharedSeg_TCB(gCellLists, gCells);
+
                 do
                 /*@ invariant 
                         mem(pxTaskItem, gCells) == true &*&
-                        xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals);
+                        xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals) &*&
+                        foreach(gCells, sharedSeg_TCB_of_itemOwner);
                  @*/
                 {
                     TCB_t * pxTCB;
@@ -1072,6 +1077,10 @@ static void prvYieldForTask( TCB_t * pxTCB,
                     //@ close xLIST_ITEM(gTaskItem_3, _, _, _, gReadyList);
                     //@ DLS_close_2(gTaskItem_3, gCells, gVals);
 
+                    // Get access to sharedSeg_TCB_p(pxTCB).
+                    //@ foreach_remove(gTaskItem_3, gCells);
+                    //@ open sharedSeg_TCB_of_itemOwner(gTaskItem_3);
+
 
                     /*debug_printf("Attempting to schedule %s on core %d\n", pxTCB->pcTaskName, portGET_CORE_ID() ); */
 
diff --git a/verification/verifast/proof/ready_list_predicates.h b/verification/verifast/proof/ready_list_predicates.h
index bd3eca7d1..d058465cc 100644
--- a/verification/verifast/proof/ready_list_predicates.h
+++ b/verification/verifast/proof/ready_list_predicates.h
@@ -3,7 +3,15 @@
 
 #include "single_core_proofs/scp_list_predicates.h"
 
+
 /*@
+// TODO: We know that the list of priority 0 is never empty.
+//       It contains the idle task and nothing else.
+predicate readyLists_p(list<list<struct xLIST_ITEM*> > gCellLists) =
+    configMAX_PRIORITIES == length(gCellLists) &*&
+    List_array_p(&pxReadyTasksLists, configMAX_PRIORITIES, gCellLists);
+
+
 predicate List_array_p(List_t* array, int size, 
                        list<list<struct xLIST_ITEM*> > cellLists) =
     size >= 0 &*&
@@ -74,12 +82,7 @@ ensures
 @*/
 
 
-/*@
-// TODO: We know that the list of priority 0 is never empty.
-//       It contains the idle task and nothing else.
-predicate readyLists_p(list<list<struct xLIST_ITEM*> > gCellLists) =
-    List_array_p(&pxReadyTasksLists, configMAX_PRIORITIES, gCellLists);
-@*/
+
 
 
 /*@
diff --git a/verification/verifast/proof/verifast_lock_predicates.h b/verification/verifast/proof/verifast_lock_predicates.h
index 640a4e07f..e949d161d 100644
--- a/verification/verifast/proof/verifast_lock_predicates.h
+++ b/verification/verifast/proof/verifast_lock_predicates.h
@@ -92,9 +92,11 @@ predicate taskISRLockInv_p() =
         integer_((void*) &uxTopReadyPriority, sizeof(UBaseType_t), false, ?gTopReadyPriority) &*&
         0 <= gTopReadyPriority &*& gTopReadyPriority < configMAX_PRIORITIES
     &*&
-    readyLists_p(?gCellLists) &*&
-    true;
-
+    readyLists_p(?gCellLists) 
+    &*&
+    // ∀gCells ∈ gCellLists. ∀item ∈ gCells. sharedSeg_TCB_p(item->pvOwner)
+    //foreach(gCellLists, foreach_sharedSeg_TCB_of_itemOwner); 
+    collection_of_sharedSeg_TCB_p(gCellLists);
 
 
 lemma void produce_taskISRLockInv();
@@ -110,6 +112,43 @@ lemma void consume_taskISRLockInv();
 requires locked_p( cons( pair(_, taskISRLockID_f()), ?otherLocks) ) &*&
          taskISRLockInv_p();
 ensures  locked_p(otherLocks);
+
+
+
+// ∀items ∈ itemLists. ∀it ∈ items. sharedSeg_TCB_p(it->pvOwner)
+predicate collection_of_sharedSeg_TCB_p(list<list<struct xLIST_ITEM*> > itemLists) =
+    foreach(itemLists, foreach_sharedSeg_TCB_of_itemOwner);
+
+// Auxiliary prediactes to express nested quantification
+// ∀gCells ∈ gCellLists. ∀item ∈ gCells. sharedSeg_TCB_p(item->pvOwner)
+// TODO: Can we refactor this to make easier to understand?
+
+    // We cannot acces `item->pvOwner` without the necessary points-to chunk.
+    // TODO: Expose list of owners in ITEM and DLS predicates.
+
+    predicate sharedSeg_TCB_of_itemOwner(struct xLIST_ITEM* item) =
+        sharedSeg_TCB_p(item->pvOwner);
+
+    predicate foreach_sharedSeg_TCB_of_itemOwner(list<struct xLIST_ITEM*> items) = 
+        foreach(items, sharedSeg_TCB_of_itemOwner);
+
+
+lemma void open_collection_of_sharedSeg_TCB(list<list<struct xLIST_ITEM*> > itemLists, 
+                                            list<struct xLIST_ITEM*> items)
+requires 
+    collection_of_sharedSeg_TCB_p(itemLists) &*&
+    mem(items, itemLists) == true;
+ensures
+    collection_of_sharedSeg_TCB_p(remove(items, itemLists)) &*&
+    foreach(items, sharedSeg_TCB_of_itemOwner);
+{
+    open collection_of_sharedSeg_TCB_p(itemLists);
+    foreach_remove(items, itemLists);
+    open foreach_sharedSeg_TCB_of_itemOwner(items);
+    close collection_of_sharedSeg_TCB_p(remove(items, itemLists));
+}
+
+// TODO: Add closing lemma
 @*/