diff --git a/algebra/sts.v b/algebra/sts.v
index c57aec2901b7da69ee2cd628b3fc16066bc63c59..6d7346321eb8b5dac2caa05409bff2163b7fb5d4 100644
--- a/algebra/sts.v
+++ b/algebra/sts.v
@@ -30,6 +30,7 @@ Inductive step : relation (state sts * tokens sts) :=
      tok s1 ∪ T1 ≡ tok s2 ∪ T2 → step (s1,T1) (s2,T2).
 Notation steps := (rtc step).
 Inductive frame_step (T : tokens sts) (s1 s2 : state sts) : Prop :=
+  (* Probably equivalent definition: (\mathcal{L}(s') ⊥ T) ∧ s \rightarrow s' *)
   | Frame_step T1 T2 :
      T1 ⊥ tok s1 ∪ T → step (s1,T1) (s2,T2) → frame_step T s1 s2.
 Notation frame_steps T := (rtc (frame_step T)).