diff --git a/program_logic/counter_examples.v b/program_logic/counter_examples.v
index 3efa5311a1a4d63af162e183d091de6a632487c0..2f63579892dab575ade2aa2030ce049ce4dd7b78 100644
--- a/program_logic/counter_examples.v
+++ b/program_logic/counter_examples.v
@@ -103,8 +103,7 @@ Module inv. Section inv.
 
   Hypothesis finished_dup : forall γ, finished γ ⊢ finished γ ★ finished γ.
 
-  (* We have that we cannot view shift from the initial state to false
-     (because the initial state is actually achievable). *)
+  (* We assume that we cannot view shift to false. *)
   Hypothesis soundness : ¬ (True ⊢ pvs1 False).
 
   (** Some general lemmas and proof mode compatibility. *)