(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
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
By:
Analyze3
Generated subgoal:
1
3.
A
4. u is the
u
:
A
.
P
(
u
)
5.
y
:
A
6.
z
:
A
7.
P
(
y
)
8.
P
(
z
)
y
=
z
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(4steps total)
PrintForm
Definitions
LogicSupplement
Sections
DiscrMathExt
Doc
Prop
!u:A. P(u)
y = z
