is mentioned by

Def termlist_eq(a;b) == Case of a; nil Case of b; nil true ; x.xs false ; x.xs Case of b; nil false ; x'.xs' term_eq(x;x')termlist_eq(xs;xs') (recursive)	[termlist_eq]
Def term_eq(a;b) == Case(a) Case x;y = > Case(b) Case x';y' = > term_eq(x;x')term_eq(y;y') Case tree_leaf(x) = > false Default = > True Case tree_leaf(x) = > Case(b) Case x';y' = > false Case tree_leaf(x') = > (x=x') Default = > True Default = > True (recursive)	[term_eq]

In prior sections: list 1 prog 1 mb basic mb nat num thy 1 mb list 1 mb tree mb automata 1

Try larger context: GenAutomata