is mentioned by

Thm* P:(TProp), A,B:T List. Thm* A = B  (i:||A||. P(A[i]))  A = B  {x:T| P(x) } List	[list-eq-set-type]
Thm* P:(TProp).  Thm* (x:T. Dec(P(x))) Thm*  Thm* (finite-type({x:T| P(x) })  (L:T List. x:T. P(x)  (x  L)))	[finite-decidable-set]
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* L:T List, P:(TProp). (xL.P(x))  L  {x:T| P(x) } List	[list-set-type2]
Thm* T:Type{i}, x:T, L:T List, P:(TTProp{i'}). Thm* (x,y[x / L].P(x,y))  (x,yL.P(x,y)) & (yL.P(x,y))	[pairwise-cons]
Thm* P:(AProp). strong-subtype(A;B)  strong-subtype({x:A| P(x) };B)	[strong-subtype-set3]
Thm* P:(AProp). strong-subtype({x:A| P(x) };A)	[strong-subtype-set2]
Thm* strong-subtype(A;B) Thm*  Thm* (P:(AProp), Q:(BProp). Thm* ((x:A. P(x)  Q(x))  strong-subtype({x:A| P(x) };{x:B| Q(x) }))	[strong-subtype-set]
Thm* A,B:Type. strong-subtype(A;B)  Prop	[strong-subtype_wf]

In prior sections: core fun 1 well fnd int 1 bool 1 int 2 list 1 mb basic rel 1 mb nat mb list 1 mb list 2

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