diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_lists_extended.h b/Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_lists_extended.h
index 147e112ae..43c6be5aa 100644
--- a/Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_lists_extended.h
+++ b/Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_lists_extended.h
@@ -10,65 +10,20 @@
 
 // TODO: Can we prove this in VeriFast or do we have to axiomatise?
 /*@
-lemma void head_drop_n_equals_nths<t>(list<t> xs, int n)
+lemma void head_drop_n_equals_nths<t>(list<t> xs, int n);
 requires n >= 0;
 ensures head(drop(n, xs)) == nth(n, xs);
-{
-    // Will prove later. For now, we only validate with an example. 
-    
-    list<int> _xs = cons(1, cons(2, cons(3, cons(4, cons(5, cons(6, cons(7, nil)))))));
-    int _n = 4;
-
-    list<int> dn = drop(_n, _xs);
-    int hdn = head(dn);
-    int nthn = nth(_n, _xs);
-    
-    assert( hdn == head(drop(_n, _xs)) );
-    assert( nthn == nth(_n, _xs ));
-    assert( head(drop(_n, _xs)) == nth(_n, _xs) );
-
-    
-    // ADMIT LEMMA, PROVE LATER
-    assume(false);
-}
 
 // TODO: Can we prove this in VeriFast or do we have to axiomatise?
-lemma void drop_index_equals_singleton_implies_last_element<t>(list<t> xs, t x)
+lemma void drop_index_equals_singleton_implies_last_element<t>(list<t> xs, t x);
 requires drop(index_of(x, xs), xs) == cons(x, nil);
 ensures index_of(x, xs) == length(xs) - 1;
-{
-    // Will prove later. For now, we only validate with an example. 
-    list<int> _xs = cons(1, cons(2, cons(3, cons(4, cons(5, cons(6, cons(7, nil)))))));
-    int _x = 7;
-
-    int i = index_of(_x, _xs);
-    list<int> d = drop(index_of(x, xs), _xs);
-
-    assert( index_of(_x, _xs) == length(_xs) - 1 );
-
-    // ADMIT LEMMA, PROVE LATER
-    assume(false);
-}
 
 // TODO: Can we prove this in VeriFast or do we have to axiomatise?
 // Can we replace this by standard lemma `drop_n_plus_one`?
-lemma void drop_cons<t>(list<t> xs, int n)
+lemma void drop_cons<t>(list<t> xs, int n);
 requires n < length(xs);
 ensures drop(n, xs) == cons(nth(n, xs), drop(n+1, xs));
-{
-    // Will prove later. For now, we only validate with an example. 
-    list<int> _xs = cons(1, cons(2, cons(3, cons(4, cons(5, cons(6, cons(7, nil)))))));
-    int _n = 3;
-
-    list<int> dn = drop(_n, _xs);
-    int nthn = nth(_n, _xs);
-    list<int> dnp1 = drop(_n + 1, _xs);
-
-    assert( drop(_n, _xs) == cons(nth(_n, _xs), drop(_n+1, _xs)) );
-
-    // ADMIT LEMMA, PROVE LATER
-    assume(false);
-}
 
 // TODO: Can we prove this in VeriFast or do we have to axiomatise?
 lemma void nth_index<t>(list<t> xs, t x)