(5steps total)
PrintForm
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa
doc
equal
via
so
A
:Type,
a
,
b
:
A
.
a
=
b
(
P
:(
A
Prop).
P
(
a
)
P
(
b
))
By:
UnivCD
Generated subgoal:
1
1.
A
: Type
2.
a
:
A
3.
b
:
A
a
=
b
(
P
:(
A
Prop).
P
(
a
)
P
(
b
))
4
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(5steps total)
PrintForm
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
A:Type, a,b:A. a = b 
(P:(A
Prop). P(a) 
P(b)) A:Type, a,b:A. a = b (P:(AProp). P(a) P(b)) a = b (P:(AProp). P(a) P(b))
