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 = t) L(SUBX(tr; S))) & RespectsNot(Tr; L) & ReflectsProp(Tr; tr; Tr)	[RepsTruth]

In prior sections: core