is mentioned by

Thm* a,b:ts(). (a=b) a = b	[assert_ts_eq]
Thm* a,b:ts(). (a=b)	[ts_eq_wf]
Thm* A:Type, v,op,f,p,t:(LabelA), x:ts(). ts_case(x)var(a)= > v(a)var'(b)= > p(b)opr(f)= > op(f)fvar(y)= > f(y)trace(P)= > t(P)end_ts_case A	[ts_case_wf]
Thm* SQType(ts())	[ts_sq]
Def Term == Tree(ts())	[term]

Try larger context: GenAutomata