Def T == {:True| T }

is mentioned by

Thm* (P  Q)  (P  Q)	[squash_functionality_wrt_iff]
Thm* (P  Q)  P  Q	[squash_functionality_wrt_implies]
Thm* SqStable(P)  (P  P)	[squash_elim]
Thm* SqStable(P)	[sq_stable__squash]
Def SqStable(P) == P  P	[sq_stable]

Try larger context: StandardLIB IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html