Nuprl - Proof: absurd nonfin imp unb inf 1 2 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: absurd nonfin imp unb inf 1 2 1 1

1. D : Type
2.

(

D)
3. Unbounded(

D)
4. f :

D
5. Inj(

D; f) [not for witness]

By:	Witness: f(0)/x,y. y

Generated subgoals:

None

About:

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