Def A == A  False

is mentioned by

Thm* b:, x,y:T. b  if b x else y fi = y	[ite_rw_false]
Thm* n:, i:{1..n}. 0 = 0 & n = 0  False	[ite_rw_test]
Thm* p:. p  p	[assert_of_bnot]
Thm* x,y:Atom. x=yAtom  x  y	[neg_assert_of_eq_atom]
Thm* x,y:. x=y  x  y	[neg_assert_of_eq_int]
Thm* b:. b  b = false	[not_assert_elim]
Thm* false	[assert_of_ff]
Thm* true = false	[btrue_neq_bfalse]

In prior sections: core

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