-| st_vref: â\88\80s,M,i. M â\93\97â\87\80*[s] #i → st M (#i)
-| st_abst: â\88\80s,M,A1,A2. M â\93\97â\87\80*[s] 𝛌.A1 → st A1 A2 → st M (𝛌.A2)
-| st_appl: â\88\80s,M,B1,B2,A1,A2. M â\93\97â\87\80*[s] @B1.A1 → st B1 B2 → st A1 A2 → st M (@B2.A2)
+| st_vref: â\88\80s,M,i. M â\93\97â\86¦*[s] #i → st M (#i)
+| st_abst: â\88\80s,M,A1,A2. M â\93\97â\86¦*[s] 𝛌.A1 → st A1 A2 → st M (𝛌.A2)
+| st_appl: â\88\80s,M,B1,B2,A1,A2. M â\93\97â\86¦*[s] @B1.A1 → st B1 B2 → st A1 A2 → st M (@B2.A2)