diff --git a/program_logic/counter_examples.v b/program_logic/counter_examples.v
index 540d3fa02eddd5faaed6bca61b9f8216e7df368f..d1fef65e9e6c4e6befa9f667f91d2adda7923363 100644
--- a/program_logic/counter_examples.v
+++ b/program_logic/counter_examples.v
@@ -156,7 +156,7 @@ Module inv. Section inv.
   Proof.
     iIntros "(#HsP & #HsQ & #HP)". iDestruct "HsP" as (i) "HiP".
     iApply (inv_open' i). iSplit; first done.
-    (* Can I state a view-shift and immediately run it? *)
+    (* TODO: How can I state a view-shift and immediately run it? *)
     iIntros "HaP". iAssert (pvs M0 (finished γ)) with "[HaP]" as "Hf".
     { iDestruct "HaP" as "[Hs | [Hf _]]".
       - by iApply start_finish.