Def x:A. B(x) == x:AB(x)

is mentioned by

Thm* l:T List, x:T. (x  l)  (l1,l2:T List. l = (l1 @ [x] @ l2))	[l_member_decomp]
Thm* ll:(T List) List, x:T. (x  concat(ll))  (l:T List. (l  ll) & (x  l))	[member-concat]
Thm* ll:(T List) List, n:||concat(ll)||. Thm* m:||ll||.  Thm* ||concat(firstn(m;ll))||n Thm* & n-||concat(firstn(m;ll))||<||ll[m]|| Thm* & concat(ll)[n] = ll[m][(n-||concat(firstn(m;ll))||)]	[select_concat]
Thm* t',m:, T:Type, f:(T), P:(T). Thm* m+1||filter(P;map(f;upto(t')))|| Thm*  Thm* (t:. P(f(t)) & ||filter(P;map(f;upto(t)))|| = m  )	[filter_map_upto2]
Thm* f:(TT'), L:T List, x',y':T'. Thm* x' before y'  map(f;L)  (x,y:T. x before y  L & f(x) = x' & f(y) = y')	[before-map]
Thm* f:(). (n:. f(n))  f(mu(f)) & (i:. i<mu(f)  f(i))	[mu-property]
Thm* f:(). (n:. f(n))  mu(f)	[mu_wf]
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* finite-type(T)  (L:T List. x:T. (x  L))	[finite-type-iff-list]
Def finite-type(T) == n:, f:(nT). Surj(n; T; f)	[finite-type]
Def strong-subtype(A;B) Def == (A r B) Def == & ({b:B| a:A. b = a  B } r A) Def == & (a1,a2:A. a1 = a2  B  a1 = a2)	[strong-subtype]

In prior sections: core fun 1 int 2 mb nat mb list 1 num thy 1 mb list 2

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