Nuprl - Proof: nonfin eqv unb inf iff negnegelim

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nonfin eqv unb inf iff negnegelim

(

A:Type.

Finite(A)

Unbounded(A))

(

P:Prop.

By:

Analyze

Generated subgoals:

1 (A:Type. Finite(A) Unbounded(A)) (P:Prop. P P)
5 steps

2 (A:Type. Finite(A) Unbounded(A)) (P:Prop. P P)
4 steps

About:

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

1	(A:Type. Finite(A) Unbounded(A)) (P:Prop. P P)	5 steps
2	(A:Type. Finite(A) Unbounded(A)) (P:Prop. P P)	4 steps