Def P  Q == (P  Q) & (P  Q)

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* 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* n:, x,y:n. x before y  upto(n)  x<y	[before-upto]
Thm* n,i:. (i  upto(n))  i<n	[member_upto]
Thm* f:(AB), l:A List. map(f;l) = nil  l = nil	[map_is_nil]
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* 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]

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 num thy 1 mb list 2

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