diff --git a/tasks.c b/tasks.c
index 1e16da104..e1f28fb0d 100644
--- a/tasks.c
+++ b/tasks.c
@@ -985,6 +985,8 @@ static void prvYieldForTask( TCB_t * pxTCB,
             //@ open taskISRLockInv();
             //@ open readyLists_p();
             //@ List_array_p_index_within_limits(&pxReadyTasksLists, uxCurrentPriority);
+            //@ List_array_get_l(pxReadyTasksLists, uxCurrentPriority);
+            //@ open xLIST(&pxReadyTasksLists[uxCurrentPriority], _, _, _, _, _);
             if( listLIST_IS_EMPTY( &( pxReadyTasksLists[ uxCurrentPriority ] ) ) == pdFALSE )
             {
                 
diff --git a/verification/verifast/proof/ready_list_predicates.h b/verification/verifast/proof/ready_list_predicates.h
index a72731d40..9b4af0ea1 100644
--- a/verification/verifast/proof/ready_list_predicates.h
+++ b/verification/verifast/proof/ready_list_predicates.h
@@ -1,17 +1,48 @@
 #ifndef READY_LIST_PREDICATES_H
 #define READY_LIST_PREDICATES_H
 
+#include "single_core_proofs/scp_list_predicates.h"
 
 /*@
-// TODO: Replace List_p by Aaloks list predicate
 predicate List_array_p(List_t* array, int size) =
-    pointer_within_limits(array) == true &*&
-    size > 0 &*&
-    List_p(array) &*&
-    size > 1
-        ? List_array_p(array + 1, size - 1)
+    size >= 0 &*&
+    size > 0
+        ? (
+            pointer_within_limits(array) == true &*&
+            xLIST(array, 
+                    ?uxNumberOfItems,
+                    ?pxIndex,
+                    ?xListEnd,
+                    ?cells,
+                    ?vals)
+            &*&
+            List_array_p(array + 1, size - 1)
+        )
         : true;
 
+lemma void List_array_get_l(List_t* array, int index)
+requires List_array_p(array, ?size) &*& 
+         0 <= index &*& index < size;
+ensures List_array_p(array, index) &*&
+        pointer_within_limits(array) == true &*&
+        xLIST(array + index, 
+                ?uxNumberOfItems,
+                ?pxIndex,
+                ?xListEnd,
+                ?cells,
+                ?vals) &*&
+        List_array_p(array + index + 1, size-index-1);
+{
+    if( index == 0) {
+        open List_array_p(array, size);
+        close List_array_p(array, 0);
+    } else {
+        open List_array_p(array, size);
+        List_array_get_l(array + 1, index - 1);
+        close List_array_p(array, index);
+    }
+}
+
 // For testing purposes only!
 // TODO: Replace by Aaloks list predicate
 predicate List_p(List_t* l);
diff --git a/verification/verifast/proof/single_core_proofs/scp_list_predicates.h b/verification/verifast/proof/single_core_proofs/scp_list_predicates.h
index 3f044594e..214db8dc2 100644
--- a/verification/verifast/proof/single_core_proofs/scp_list_predicates.h
+++ b/verification/verifast/proof/single_core_proofs/scp_list_predicates.h
@@ -212,6 +212,8 @@ ensures DLS(n, nprev, mnext, m, cells, vals, l) &*& distinct(cells) == true;
 	}
 }
 
+#endif /* VERIFAST_TODO */
+/*@
 predicate xLIST(
 	struct xLIST *l,
 	int uxNumberOfItems,
@@ -229,7 +231,9 @@ predicate xLIST(
 	length(cells) == length(vals) &*&
 	uxNumberOfItems + 1 == length(cells) &*&
 	DLS(xListEnd, ?endprev, xListEnd, endprev, cells, vals, l);
+@*/
 
+#ifdef VERIFAST_TODO
 lemma void xLIST_distinct_cells(struct xLIST *l)
 requires xLIST(l, ?n, ?idx, ?end, ?cells, ?vals);
 ensures xLIST(l, n, idx, end, cells, vals) &*& distinct(cells) == true;