is mentioned by

Def niltrace() == mk_trace_env(nil, P,k. false)	[niltrace]
Def st_eq(s1;s2) == Case(s1) Case a;b = > Case(s2) Case a';b' = > st_eq(a;a')st_eq(b;b') Default = > false Case tree_leaf(x) = > Case(s2) Case a';b' = > false Case tree_leaf(y) = > InjCase(x; x'. InjCase(y; y'. x' = y'; b. false); a. InjCase(y; y'. false; b. true)) Default = > false Default = > false (recursive)	[st_eq]
Def (a=b) == ts_case(a) var(v)= > ts_case(b) var(v')= > v = v' var'(x)= > false opr(x)= > false fvar(x)= > false trace(x)= > false end_ts_case var'(p)= > ts_case(b) var(x)= > false var'(p')= > p = p' opr(x)= > false fvar(x)= > false trace(x)= > false end_ts_case opr(op)= > ts_case(b) var(x)= > false var'(x)= > false opr(op')= > op = op' fvar(x)= > false trace(x)= > false end_ts_case fvar(f)= > ts_case(b) var(x)= > false var'(x)= > false opr(x)= > false fvar(f')= > f = f' trace(x)= > false end_ts_case trace(P)= > ts_case(b) var(x)= > false var'(x)= > false opr(x)= > false fvar(x)= > false trace(P')= > P = P' end_ts_case end_ts_case	[ts_eq]

In prior sections: bool 1 sqequal 1 prog 1 mb basic list 1 union mb label mb tree

Try larger context: GenAutomata