IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
nonfin eqv unb inf iff negnegelim1211 1. A:Type. Finite(A) Unbounded(A)
2. D:Type. (D) (D)
3. P : Prop
4. A : Type
5. P = (A)
(A) (A)
By:
Witness2: A
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
A:Type. 
Finite(A) 
Unbounded(A)
D) 
