(4steps total)
PrintForm
Definitions
LogicSupplement
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
exists
unique
elim
A
:Type,
P
:(
A
Prop). (
!
u
:
A
.
P
(
u
))
(
y
,
z
:
A
.
P
(
y
)
P
(
z
)
y
=
z
)
By:
Auto
Generated subgoal:
1
1.
A
: Type
2.
P
:
A
Prop
3.
!
u
:
A
.
P
(
u
)
4.
y
:
A
5.
z
:
A
6.
P
(
y
)
7.
P
(
z
)
y
=
z
3
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(4steps total)
PrintForm
Definitions
LogicSupplement
Sections
DiscrMathExt
Doc
A:Type, P:(A
Prop). (
!u:A. P(u)) 
(y,z:A. P(y) P(z) y = z) A:Type, P:(AProp). (!u:A. P(u)) (y,z:A. P(y) P(z) y = z)Prop
!u:A. P(u)
y = z
