Def A == A  False

is mentioned by

Thm* 'a:S, l:'a List. mt(l)  cons(head(l); tl(l)) = l	[cons_char]
Thm* 'a:S, h1,h2:'a. h1 = h2  (l1,l2:'a List. cons(h1; l1) = cons(h2; l2))	[not_eq_list]
Thm* 'a:S, l1,l2:'a List. l1 = l2  (h1,h2:'a. cons(h1; l1) = cons(h2; l2))	[list_not_eq]
Thm* 'a:S, t:'a List, h:'a. cons(h; t) = nil	[not_cons_nil]
Thm* 'a:S, t:'a List, h:'a. nil = cons(h; t)	[not_nil_cons]

In prior sections: core bool 1 int 2 list 1 hol hol bool hol num hol prim rec hol list 1

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