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