(8steps total)
PrintForm
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa
doc
inlist
singleton
const
A
:Type,
a
:
A
,
w
:{
a
:
A
} List,
z
:
A
.
z
list
w
z
=
a
By:
Guarding (
w
:{
a
:
A
} List. <prop>) UnivCD
Generated subgoal:
1
1.
A
: Type
2.
a
:
A
w
:{
a
:
A
} List,
z
:
A
.
z
list
w
z
=
a
7
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(8steps total)
PrintForm
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
A:Type, a:A, w:{a:A} List, z:A. z 
list w 
z = a A:Type, a:A, w:{a:A} List, z:A. z list w z = aw:{a:A} List. <prop>) UnivCD w:{a:A} List, z:A. z list w z = a
