Def A == A  False

is mentioned by

Thm* R:(TTProp).  Thm* (x,y:T. Dec(R(x,y))) Thm*  Thm* Linorder(T;x,y.R(x,y))  (a,b:T. strict_part(x,y.R(x,y);a;b)  R(b,a))	[linorder_lt_neg]
Thm* R:(TTProp).  Thm* Linorder(T;x,y.R(x,y))  (a,b:T. R(a,b)  strict_part(x,y.R(x,y);b;a))	[linorder_le_neg]
Thm* R:(TTProp), a,b:T. strict_part(x,y.R(x,y);a;b)  a = b	[strict_part_irrefl]
Def Irrefl(T;x,y.E(x;y)) == a:T. E(a;a)	[irrefl]
Def strict_part(x,y.R(x;y);a;b) == R(a;b) & R(b;a)	[strict_part]
Def StAntiSym(T;x,y.R(x;y)) == x,y:T. (R(x;y) & R(y;x))	[st_anti_sym]

In prior sections: core bool 1

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