Nuprl - Proof: unique fn over empty 1 2

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

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

(

A)
4. y : A

(

x.x) = y

By:	FunExtensionality

Generated subgoals:

1 5. x : A
x = y(x) B
1 step

2 5. x : A
x B
1 step

About:

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