Def SqStable(P) == P  P

is mentioned by

Thm* SqStable(P)  (P  P)	[squash_elim]
Thm* Dec(P)  SqStable(P)	[sq_stable_from_decidable]
Thm* SqStable(P)	[sq_stable__not]
Thm* Stable{P}  SqStable(P)	[sq_stable__from_stable]
Thm* SqStable(P)	[sq_stable__squash]
Thm* x,y:A. SqStable(x = y)	[sq_stable__equal]
Thm* P:(AProp). (x:A. SqStable(P(x)))  SqStable(x:A. P(x))	[sq_stable__all]
Thm* SqStable(P)  SqStable(Q)  SqStable(P  Q)	[sq_stable__iff]
Thm* SqStable(Q)  SqStable(P  Q)	[sq_stable__implies]
Thm* SqStable(P)  SqStable(Q)  SqStable(P & Q)	[sq_stable__and]

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