Def  A == A

is mentioned by

Thm*  ((a onto b))  ba	[surj_typing_imp_le]
Thm*  ((a onto b))  ((b inj a))	[nsub_surj_imp_a_rev_inj2]
Thm*  ((AB)) ~ (A ~ B)	[inv_pair_inv2]
Thm*  (A:Type. Finite(A)  Infinite(A))  (D:Type. (D)  (D))	[absurd_nonfinite_imp_infinite]
Thm*  (A:Type. Finite(A)  Unbounded(A))  (D:Type. (D)  (D))	[absurd_nonfin_imp_unb_inf]
Thm*  (A ~ B)  ((A)  (B))	[inhabited_functionality_wrt_one_one_corr]
Thm*  ((AB))  (A ~ B)	[inv_pair_iff_ooc]
Thm*  P:{P:(Prop)| i:. P(i) }.  Thm*  (i:. Dec(P(i)))  ({i:| P(i) & (j:. j<i  P(j)) })	[least_exists2]
Thm*  k:, P:{P:(kProp)| i:k. P(i) }. Thm*  (i:k. Dec(P(i)))  ({i:k| P(i) & (j:i. P(j)) })	[least_exists]
Thm*  (A ~ 0)  (A)	[card0_iff_uninhabited]
Thm*  (A:Type, R:(AAProp). Thm*  ((A) & (Trans x,y:A. R(x;y)) & (x:A. y:A. R(x;y)) Thm*  (& (x:A. R(x;x)) Thm*  (& Finite(A))	[no_finite_model]
Thm*  R:(AAProp).  Thm*  (A) & (Trans x,y:A. R(x;y)) & (x:A. y:A. R(x;y)) Thm*   Thm*  (k:. f:(kA). i,j:k. i<j  R(f(i);f(j)))	[no_finite_model_lemma]
Thm*  ((m inj k))  mk	[inj_typing_imp_le]
Thm*  (A)  (!(A inj B))	[inj_from_empty_unique]
Thm*  ((A inj B))  (f:(AB). Inj(A; B; f))	[injtype_vs_inj]
Def  Infinite(A) == ( inj A)	[productively_infinite]
Def  Unbounded(A) == k:. (k inj A)	[unboundedly_infinite]

In prior sections: LogicSupplement

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