Nuprl - Proof: unb inf not fin 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: unb inf not fin 1 1 1 1

1. A : Type
2. Unbounded(A)
3. n :

4. A ~

n
5.

(

(n+1) inj

A)
6.

(

(n+1) inj

False

By:	FwdThru: Thm* ((m inj k)) mk on [ Hyp:-1 ]

Generated subgoals:

None

About:

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