Def A == A  False

is mentioned by

Thm* ((n.n<0) ~ (n.false))	[sfa_doc_sqtype_ctr_example_part1]
Thm* A  (C:Prop. A  C)	[sfa_doc_not_via_so]
Thm* f:{f:()| x:. f(x) }, i:. i<mu(f)  f(i)	[kleene_minimize_is_lb]
Thm* f:{f:()| x:. f(x) }. f(0)  (x.f(1+x))  {f:()| x:. f(x) }	[kleene_tail]

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

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html