Def SqStable(P) == P  P

is mentioned by

Thm* P:(TProp).  Thm* (x:T. SqStable(P(x))) Thm*  Thm* (finite-type({x:T| P(x) })  (L:T List. x:T. P(x)  (x  L)))	[finite-set-type]
Thm* SqStable(A r B)	[sq_stable__subtype_rel]

In prior sections: core fun 1 rel 1 num thy 1

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