is mentioned by

Thm* t:Term. s(t) = SUBX(t; s(t))	[s_reps]
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]