STSs: Consider changing the def. of frame-steps
Jeehoon wrote on the iris-club list:
the definition of s \stackrel{T}{\rightarrow} s' involves the existential quantification of T1 and T2, and I think there exists an alternative definition that does not involve that quantification: $(\mathcal{L}(s') # T) /\ s \rightarrow s' .$ This is obtained by letting T1 and T2 be (\mathcal{L}(s') \setminus \mathcal{L}(s)) and (\mathcal{L}(s) \setminus \mathcal{L}(s')).
We could change frame_step accordingly, maybe this simplifies some things a little.