is mentioned by

Thm* B (A B & C) (A C)	[prop_and_iff]
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 RespectsNot(Tr; L) == t:Term. Tr(NOT(t)) L(t) & Tr(t)	[RespectsNot]

In prior sections: core