S:Term. (
t:Term. S 
= t) 
L(SUBX(tr; S))) & RespectsNot(Tr; L) & ReflectsProp(Tr; tr; Tr)t:Term. Tr(NOT(t)) 
L(t) & 
Tr(t)
is mentioned by
| Def RepsTruth(L; Tr; tr) == (S:Term. (t:Term. S = t) L(SUBX(tr; S))) & RespectsNot(Tr; L) & ReflectsProp(Tr; tr; Tr) | [RepsTruth] |