Def A == A  False

is mentioned by

Thm* as:A List. as = nil  ||as||1	[length_of_not_nil]
Thm* l:A List. l = nil  ||l||1	[pos_length]
Thm* h:T, t:T List. h.t = nil	[cons_neq_nil]

In prior sections: core bool 1 int 2

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