diff --git a/program_logic/counter_examples.v b/program_logic/counter_examples.v
index 3b1751aa91a61a0cdf01eedb0cf9f6b3f9d9f141..540d3fa02eddd5faaed6bca61b9f8216e7df368f 100644
--- a/program_logic/counter_examples.v
+++ b/program_logic/counter_examples.v
@@ -87,6 +87,12 @@ Module inv. Section inv.
   (* We have tokens for a little "two-state STS": [start] -> [finish].
      state. [start] also asserts the exact state; it is only ever owned by the
      invariant.  [finished] is duplicable. *)
+  (* Posssible implementations of these axioms:
+     * Using the STS monoid of a two-state STS, where [start] is the
+       authoritative saying the state is exactly [start], and [finish]
+       is the "we are at least in state [finish]" typically owned by threads.
+     * Ex () +_⊥ ()
+  *)
   Context (gname : Type).
   Context (start finished : gname → iProp).