is mentioned by

Thm* s1,s2:SimpleType. st_eq(s1;s2) s1 = s2	[assert_st_eq]
Thm* a,b:ts(). (a=b) a = b	[assert_ts_eq]

In prior sections: bool 1 list 1 mb basic mb nat union mb list 1 mb label mb tree mb list 2 rel 1

Try larger context: GenAutomata