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

is mentioned by

Thm* a:Id, l:IdLnk, tg:Id. locl(a) = rcv(l; tg)  False	[not_locl_rcv]
Thm* a:Id, l:IdLnk, tg:Id. rcv(l; tg) = locl(a)  False	[not_rcv_locl]
Thm* a,b:Id. locl(a) = locl(b)  a = b	[locl_one_one]
Thm* k:Knd. islocal(k) ~ isrcv(k)	[islocal-not-isrcv]
Thm* l:IdLnk. lnk-inv(lnk-inv(l)) = l  IdLnk	[lnk-inv-inv]
Thm* f:((T List)), t,t':. Thm* t<t'  concat(map(f;upto(t))) @ (f(t))  concat(map(f;upto(t')))	[concat_map_upto]
Thm* ll1,ll2:(T List) List. ll1  ll2  concat(ll1)  concat(ll2)	[concat_iseg]
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* l:Top List, ll:(Top List) List. concat([l / ll]) ~ (l @ concat(ll))	[concat-cons]
Thm* ll1,ll2:(Top List) List. concat(ll1 @ ll2) ~ (concat(ll1) @ concat(ll2))	[concat_append]
Thm* n,m:. firstn(n;upto(m)) ~ if nm upto(n) else upto(m) fi	[firstn_upto]
Thm* f:(TopTop), n:, l:Top List. firstn(n;map(f;l)) ~ map(f;firstn(n;l))	[firstn_map]
Thm* L:Top List, n:. ||L||n  (firstn(n;L) ~ L)	[firstn_all]
Thm* L1,L2:Top List, n:(||L1||+1). firstn(n;L1 @ L2) ~ firstn(n;L1)	[firstn_append]
Thm* L:Top List. firstn(0;L) ~ nil	[first0]
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* i,j:. Thm* i<j Thm*  Thm* (f:(T), P:(T). Thm* (P(f(i))  ||filter(P;map(f;upto(i)))||<||filter(P;map(f;upto(j)))||)	[filter_map_upto]
Thm* P:(T), A:T List, B:Top. filter(P;A @ B) ~ (filter(P;A) @ filter(P;B))	[filter_append_sq]
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* 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* n:, x,y:n. x before y  upto(n)  x<y	[before-upto]
Thm* n,i:. i<n  (i  upto(n))	[member_upto2]
Thm* n,i:. (i  upto(n))  i<n	[member_upto]
Thm* m:, n:m. upto(m)[n] = n	[select_upto]
Thm* i,j:. ij  upto(i)  upto(j)	[upto_iseg]
Thm* m:, n:(m+1). upto(m) ~ (upto(n) @ map(x.x+n;upto(m-n)))	[upto_decomp]
Thm* n:. ||upto(n)|| ~ n	[length_upto]
Thm* n:. upto(n)  n List	[upto_wf]
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* r:, L:Top List. ||nth_tl(r;L)|| = if r<||L|| ||L||-r else 0 fi	[general_length_nth_tl]
Thm* f:Top, T:Type, L:T List, i:||L||. map(f;L)[i] ~ (f(L[i]))	[select-map]
Thm* f:Top, T:Type, L:T List. ||map(f;L)|| ~ ||L||	[length-map]
Thm* L:Top List. map(x.x;L) ~ L	[map-id]
Thm* f:(AB), l:A List. map(f;l) = nil  l = nil	[map_is_nil]
Thm* as:Top List, f,g:Top. map(g;map(f;as)) ~ map(g o f;as)	[map-map]
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]
Thm* x:A, y:B. inl(x) = inr(y)  A+B  False	[inl_eq_inr]
Thm* as,bs,cs:Top List. ((as @ bs) @ cs) ~ (as @ bs @ cs)	[append_assoc_sq]
Thm* L:T List, P:(TProp). (xL.P(x))  L  {x:T| P(x) } List	[list-set-type2]
Thm* L:T List. L  {x:T| (x  L) } List	[list-set-type]
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* l:T List, i:||l||, j:i. last(l_interval(l;j;i)) = l[(i-1)]	[last_l_interval]
Thm* l:T List, i:||l||, j:i. hd(l_interval(l;j;i)) = l[j]	[hd_l_interval]
Thm* l:T List, i:||l||, j:(i+1), x:(i-j). l_interval(l;j;i)[x] = l[(j+x)]	[select_l_interval]
Thm* l:T List, i:||l||, j:(i+1). ||l_interval(l;j;i)|| = i-j	[length_l_interval]
Thm* L:A List, x:A. (A r B)  (x  L)  (x  L)	[l_member_subtype]
Thm* f:(A), L:A List. 0<||L||  (aL.(xL.f(x)f(a)))	[maximal-in-list]
Thm* n,m:, f,i:Top. (f^n+m(i)) ~ (f^n(f^m(i)))	[fun_exp_add_sq]
Thm* SqStable(A r B)	[sq_stable__subtype_rel]
Thm* strong-subtype(A;B)  (L:A List, x:B. (x  L)  (x  L))	[strong-subtype-l_member]
Thm* strong-subtype(A;B)  (L:A List, x:B. (x  L)  x  A)	[strong-subtype-l_member-type]
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 r A	[subtype_rel_self]
Thm* strong-subtype(A;B)  strong-subtype(B;C)  strong-subtype(A;C)	[strong-subtype_transitivity]
Thm* strong-subtype(A;A)	[strong-subtype-self]
Thm* A,B:Type. strong-subtype(A;B)  Prop	[strong-subtype_wf]
Thm* (A r B)  (B r C)  (A r C)	[subtype_rel_transitivity]
Thm* (A r B)  ((A List) r (B List))	[subtype_rel_list]
Thm* B:(AType), C:Type, D:(CType). Thm* (A r C)  (a:A. B(a) r D(a))  ((a:AB(a)) r (c:CD(c)))	[subtype_rel_product]
Thm* B:(AType), C:Type, D:(CType). Thm* (C r A)  (a:C. B(a) r D(a))  ((a:AB(a)) r (c:CD(c)))	[subtype_rel_dep_function]
Thm* (C r A)  (B r D)  ((AB) r (CD))	[subtype_rel_function]
Thm* x,y:A. (A r B)  x = y  x = y  B	[equal_functionality_wrt_subtype_rel]
Def (x,yL.P(x;y)) == i:||L||, j:i. P(L[j];L[i])	[pairwise]
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 well fnd int 1 bool 1 int 2 list 1 sqequal 1 union mb basic rel 1 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