At: nsub inj discr range bijtype

  A:Type. 
  (A Discrete)  (k:, f:(k inj A). f  k bij {a:A| i:k. a = f(i) })

By:	SimilarTo: 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)) THEN ExistHD Hyp:-1

1

1. A : Type 2. A Discrete 3. k :  4. f : k inj A 5. {a:A| i:k. a = f(i) }  Type 6. f  k{a:A| i:k. a = f(i) } 7. Bij(k; {a:A| i:k. a = f(i) }; f)   f  k bij {a:A| i:k. a = f(i) }

1 step

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html