is mentioned by

Thm* t1,t2:Term. closed_term(t1 t2) closed_term(t1) & closed_term(t2)	[closed_tapp]
Def term_subst2(as;t) == iterate(statevar v- > v statevar v'- > apply_alist(as;v;v') funsymbol f- > f freevar f- > f trace(P)- > trace(P) x(y)- > x y over t)	[term_subst2]
Def (t)' == term_iterate(x.x';x.x';op.op;f.f;P.trace(P);a,b. a b;t)	[addprime]
Def term_subst(as;t) == iterate(statevar v- > apply_alist(as;v;v) statevar v'- > apply_alist(as;v;v') funsymbol f- > f freevar f- > f trace(P)- > trace(P) x(y)- > x y over t)	[term_subst]
Def unprime(t) == term_iterate(x.x;x.x;op.op;f.f;P.trace(P);a,b. a b;t)	[unprime]

Try larger context: GenAutomata