Def A == A  False

is mentioned by

Thm* k:, P:(k). Thm* ((i:k. P(i))  0<search(k;P)) Thm* & (0<search(k;P)  P(search(k;P)-1) & (j:k. j<search(k;P)-1  P(j)))	[search_property]
Thm* n,m:, f:(nm), x1,x2:n, y1,y2:m. Thm* x1 = x2  y1 = y2 Thm*  Thm* (x:n, y:m. (x = x1 & y = y1)  (x = x2 & y = y2)  f(x,y) = 0) Thm*  Thm* sum(f(x,y) | x < n; y < m) = f(x1,y1)+f(x2,y2)	[pair_support_double_sum]
Thm* n:, f:(n), m,k:n. Thm* m = k Thm*  Thm* (x:n. x = m  x = k  f(x) = 0)  sum(f(x) | x < n) = f(m)+f(k)	[pair_support]
Thm* n:, f:(n), m:n. Thm* (x:n. x = m  f(x) = 0)  sum(f(x) | x < n) = f(m)	[singleton_support_sum]
Thm* m:, P:(mProp). Thm* (i:m. Dec(P(i))) Thm*  Thm* (n,k:, f:(nm), g:(km). Thm* (increasing(f;n) Thm* (& increasing(g;k) Thm* (& (i:n. P(f(i))) Thm* (& (j:k. P(g(j))) Thm* (& (i:m. (j:n. i = f(j))  (j:k. i = g(j))))	[increasing_split]
Thm* m,n,k:, f:(nm), g:(km). Thm* increasing(f;n) Thm*  Thm* increasing(g;k) Thm*  Thm* (i:m. (j:n. i = f(j))  (j:k. i = g(j))) Thm*  Thm* (j1:n, j2:k. f(j1) = g(j2))  m = n+k	[disjoint_increasing_onto]

In prior sections: core bool 1 int 2 list 1 rel 1 sqequal 1

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