is mentioned by

Thm* v:Top, rho:Decl. v [[ < > ]] rho	[empty_sts_mng]
Def st_app1(s1;s2) == Case(s1) Case a;b = > if st_eq(a;s2) < b > else < > fi Default = > < >	[st_app1]

In prior sections: mb collection

Try larger context: GenAutomata