Def  A Discrete == x,y:A. Dec(x = y)

is mentioned by

Thm*  f:(A onto B), a:. a onto A  (B Discrete)  Surj(A; B; f)	[surjection_type_surjection]
Thm*  (A Discrete)  (k:, f:(k inj A). f  k bij {a:A| i:k. a = f(i) })	[nsub_inj_discr_range_bijtype]
Thm*  (A Discrete) Thm*   Thm*  (k:, f:(k inj A). Thm*  ({a:A| i:k. a = f(i) }  Type Thm*  (& f  k{a:A| i:k. a = f(i) } Thm*  (& Bij(k; {a:A| i:k. a = f(i) }; f))	[nsub_inj_discr_range_bij]
Thm*  (A Discrete)  (k:, f:(kA). f  k onto {a:A| i:k. a = f(i) })	[nsub_discr_range_surjtype]
Thm*  (A Discrete) Thm*   Thm*  (k:, f:(kA). Thm*  ({a:A| i:k. a = f(i) }  Type Thm*  (& f  k{a:A| i:k. a = f(i) } Thm*  (& Surj(k; {a:A| i:k. a = f(i) }; f))	[nsub_discr_range_surj]

In prior sections: LogicSupplement

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