is mentioned by

Thm* (Tr:(TermProp), tr:Term, L:(TermProp). RepsTruth(L; Tr; tr))	[Tarski]
Def RepsTruth(L; Tr; tr) == (S:Term. (t:Term. S reps t) L(tr/S)) & RespectsNot(Tr; L) & ReflectsProp(Tr; tr; Tr)	[RepsTruth]

In prior sections: core