S:Term. (
t:Term. S 
= t) 
L(SUBX(tr; S))) & RespectsNot(Tr; L) & ReflectsProp(Tr; tr; Tr)t,qt:Term. qt = t {Tr(SUBX(qP; qt)) 
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] |