is mentioned by

Thm* a,b:Term List. termlist_eq(a;b)	[termlist_eq_wf]
Thm* a,b:relname(). eq_relname(a;b)	[eq_relname_wf]
Thm* a,b:Term. term_eq(a;b)	[term_eq_wf]

In prior sections: bool 1 sqequal 1 list 1 rel 1 mb basic mb nat mb list 1 mb events mb tree mb list 2 mb automata 1 prog 1

Try larger context: GenAutomata