(A:Type. Finite(A)  Unbounded(A))  (P:Prop. P  P)

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

1

1. P:Prop. P  P 2. A : Type 3. Finite(A)  Unbounded(A)   Finite(A)  Unbounded(A)

3 steps

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