(A:Type. Finite(A)  Infinite(A))  (D:Type. (D)  (D))

By:	SimilarTo: Thm*  (A:Type. Finite(A)  Unbounded(A))  (D:Type. (D)  (D))

1

1. A : Type 2. Finite(A) 3. Infinite(A)   Unbounded(A)

1 step

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