Def T == {:True| T }

is mentioned by

Thm* E:(TTProp). (EquivRel x,y:T. E(x,y))  (EquivRel x,y:T. E(x,y))

[squash_thru_equiv_rel]

In prior sections: core

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