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

is mentioned by

Thm* l:T List, x:T. no_repeats(T;[x / l])  no_repeats(T;l) & (x  l)	[no_repeats_cons]
Thm* l:T List. no_repeats(T;l)  (x,y:T. x before y  l  x = y)	[no_repeats_iff]
Thm* L:T List. L  nil  null(L)	[iseg_nil]
Thm* l1,l2:T List. l1  l2  ||l1||||l2|| & (i:. i<||l1||  l1[i] = l2[i])	[iseg_select]
Thm* L1,L2:T List. L1  L2  (n:(||L2||+1). L1 = firstn(n;L2))	[firstn_is_iseg]
Thm* a,b:T, l1,l2:T List. [a / l1]  [b / l2]  a = b & l1  l2	[cons_iseg]
Thm* P:(T), L:T List, x:T. (x  filter(P;L))  (x  L) & P(x)	[member_filter]
Thm* l:T List, a,x,y:T. Thm* x before y  [a / l]  x = a & (y  l)  x before y  l	[cons_before]
Thm* x,y:T. x before y  nil  False	[nil_before]
Thm* x:T, L:T List. (x  L)  [x]  L	[member_iff_sublist]
Thm* L:T List. L  nil  L = nil	[sublist_nil]
Thm* x1,x2:T, L1,L2:T List. Thm* [x1 / L1]  [x2 / L2]  x1 = x2 & L1  L2  [x1 / L1]  L2	[cons_sublist_cons]
Thm* L:T List. nil  L  True	[nil_sublist]
Thm* x:T, L:T List. [x / L]  nil  False	[cons_sublist_nil]
Thm* a:T List, x:T', f:(TT'). (x  map(f;a))  (y:T. (y  a) & x = f(y))	[member_map]
Thm* a,x:T. (x  [a])  x = a	[member_singleton]
Thm* x:T, l1,l2:T List. (x  l1 @ l2)  (x  l1)  (x  l2)	[member_append]
Thm* l:T List, a,x:T. (x  [a / l])  x = a  (x  l)	[cons_member]
Thm* x:T. (x  nil)  False	[nil_member]
Thm* l1,l2:T List. (l1 @ l2) = nil  l1 = nil & l2 = nil	[append_is_nil]
Thm* a,a':T, b,b':T List. [a / b] = [a' / b']  a = a' & b = b'	[cons_one_one]
Thm* l:T List. ||l|| = 0    l = nil	[length_zero]
Thm* L:T List, P:(||L||Prop). Thm* (x:||L||. Dec(P(x))) Thm*  Thm* (i,j:||L||. P(i)  i<j  P(j)) Thm*  Thm* (L_1,L_2:T List. L = (L_1 @ L_2) & (i:||L||. P(i)  ||L_1||i))	[append_split2]

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

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