(2steps total)
PrintForm
Definitions
mb
list
1
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
length
zero
T
:Type,
l
:
T
List. ||
l
|| = 0
l
= nil
By:
UnivCD THEN Analyze -1 THEN Reduce 0
Generated subgoal:
1
1.
T
: Type
2.
u
:
T
3.
v
:
T
List
4. [
u
/
v
] = nil
||
v
||+1 = 0
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
mb
list
1
Sections
MarkB
generic
Doc
T:Type, l:T List. ||l|| = 0 
l = nil T:Type, l:T List. ||l|| = 0 l = nil ||v||+1 = 0
