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,e:Term. SUBX(NOT(t); e) = NOT(SUBX(t; e))	[qnot_subx]
Thm* t,r,t',r':Term. t = t' & r = r' SUBX(t; r) = SUBX(t'; r')	[qsubx_repst]
Def RepsTruth(L; Tr; tr) == (S:Term. (t:Term. S = t) L(SUBX(tr; S))) & RespectsNot(Tr; L) & ReflectsProp(Tr; tr; Tr)	[RepsTruth]
Def ReflectsProp(P; qP; Tr) == t,qt:Term. qt = t {Tr(SUBX(qP; qt)) Tr(t)}	[ReflectsProp]
Def s(t) == SUBX(f(t); f(t))	[s]