Nuprl - Proof: exists unique elim 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: exists unique elim 1 1

1. A : Type
2. P : A

Prop
3. A
4. u is the u:A. P(u)
5. y : A
6. z : A
7. P(y)
8. P(z)

y = z

By:	FwdThru: Hyp:4 on [ P(y) ] THEN FwdThru: Hyp:4 on [ P(z) ]

Generated subgoal:

1 9. y = u
10. z = u
y = z
Trivial

About:

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