Def A == A  False

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* L1,L2:T List. null(L2)  L1  tl(L2)  L1  L2	[sublist_tl]
Thm* L:T List, x:T. null(L)  last([x / L]) = last(L)	[last_cons]
Thm* T:Type, L:T List. null(L)  last(L)  T	[last_wf]
Thm* L:T List, x:T. (x  L)  null(L)	[member_null]
Thm* L:T List, x:T. null(L)  (x  L)	[null_member]
Thm* L:T List. L = nil  (x:T. (x  L))	[member_exists]
Thm* L:T List. L = nil  0<||L||	[non_nil_length]
Def no_repeats(T;l) == i,j:. i<||l||  j<||l||  i = j  l[i] = l[j]  T	[no_repeats]

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

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