is mentioned by

Thm* t:Term. s(t) = SUBX(t; SUBX(f(t); f(t)))	[s2]
Thm* t:Term. s(t) = SUBX(t; SUBX(f(t); UP(f(t))))	[s1]
Def s(t) == SUBX(f(t); f(t))	[s]