is mentioned by

Thm* as:(LabelT) List, p:(LabelT), l:Label, d:T. apply_alist([p / as];l;d) ~ if 1of(p) = l 2of(p) else apply_alist(as;l;d) fi	[apply_alist_cons]
Def apply_alist(as;l;d) == 2of((first p as s.t. 1of(p) = l else < l,d > ))	[apply_alist]
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: mb basic mb label mb declaration

Try larger context: GenAutomata