is mentioned by

Thm* (Tr:(TermProp), tr:Term, L:(TermProp). RepsTruth(L; Tr; tr))	[Tarski]
Thm* (P P) False	[prop_iff_contra]
Def RespectsNot(Tr; L) == t:Term. Tr(NOT(t)) L(t) & Tr(t)	[RespectsNot]

In prior sections: core