+interpretation "'st' computation"
+ 'Std M N = (st M N).
+
+notation "hvbox( M ⓢ⥤* break term 46 N )"
+ non associative with precedence 45
+ for @{ 'Std $M $N }.
+
+axiom st_refl: reflexive … st.
+
+axiom st_step_sn: ∀N1,N2. N1 ⓢ⥤* N2 → ∀s,M. M ⓗ⇀*[s] N1 → M ⓢ⥤* N2.
+
+axiom st_lift: liftable st.
+
+axiom st_inv_lift: deliftable_sn st.
+
+axiom st_dsubst: dsubstable st.