Def  A == A  False

is mentioned by

Thm*  e:(BB).  Thm*  (b:B. e(b) = b) Thm*   Thm*  (A:Type, f:(AAB). (a:A. (Diag f wrt x. e(x)) = f(a)))	[diagonalization_wrt_eq]
Thm*  R:(BBProp), e:(BB). Thm*  (b:B. R(e(b),b)) Thm*   Thm*  (A:Type, f:(AAB). (a:A. R((Diag f wrt x. e(x))(a),f(a,a))))	[diagonalization]
Thm*  (Set:Type, :(SetSetProp). Thm*  (P:(SetProp). p:Set. x:Set. (x  p)  P(x))	[RussellsParadox_Frege2]
Thm*  (A:Type, Q:(AAProp). P:(AProp). p:A. x:A. Q(x,p)  P(x))	[RussellsParadox_Frege]
Thm*  (P  P)	[no_prop_iff_its_neg]
Thm*  P XOR Q  (Q  P) & Dec(P)	[xor_vs_neg_n_dec]
Thm*  (P)  P	[sq_not_iff_sq]
Thm*  P  P	[not_sq_iff_sq]
Thm*  (A)  (!(AB))	[unique_fn_over_empty]
Thm*  (x:T. Q(x))  (x:T. Q(x))	[not_over_exists_imp]
Thm*  P  Q  P  Q	[disjunct_elim]
Thm*  (P:Prop. P  P)  (P:Prop. P  P)	[negnegelim_vs_bivalence]
Def  P XOR Q == P  Q & (P & Q)	[xor]

In prior sections: core bool 1 rel 1

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