diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/README.md b/Test/VeriFast/tasks/vTaskSwitchContext/README.md
index 561603fd659..46cfc3e3561 100644
--- a/Test/VeriFast/tasks/vTaskSwitchContext/README.md
+++ b/Test/VeriFast/tasks/vTaskSwitchContext/README.md
@@ -198,6 +198,16 @@ Both scripts expect the command line arguments explained below.
   - \<FONT_SIZE\> is an optional argument specifying the IDE's font size.
 
 
+# Reading the Proof
+The most important parts that we have to understand in order to understand what the proof are the following, in this order:
+  - The locking discipline, cf. `proof/port_locking_contracts.h`
+  - The lock invariants, cf. `proof/lock_predicates.h`. The invariants use the ready list and task predicates defined in `proof/ready_list_predicates.h` and `task_predicates.h`.
+  - The contracts for the functions we verified, i.e., `vTaskSwitchContext` and `prvSelectHighestPriorityTask`, cf. `src/tasks.c`.
+We propose to first skim the files mentioned above, in the provided order to get an overview of how the proof is structured.
+
+
+
+
 # Maintaining the Proof
 This directory contains annotated copies of FreeRTOS source and header files.
 The annotations in these files tell VeriFast which functions it should verify and what the proof looks like.