is mentioned by

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

In prior sections: mb automata 1

Try larger context: GenAutomata