is mentioned by

Thm* t:Term. s(t) reps t/s(t)	[s_reps]
Thm* t:Term. s(t) reps t/(f(t)/q(f(t)))	[s2]
Thm* t:Term. s(t) = SUBX(q(t); SUBX(q(f(t)); Q(q(f(t)))))	[s1]