Nuprl - Proof: unique fn over empty 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: unique fn over empty 1

1. A : Type
2. B : Type
3.

(

By:	Witness: x.x

Generated subgoals:

1 4. x : A
x B
1 step

2 4. y : AB
(x.x) = y
3 steps

About:

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