(4steps total)
PrintForm
Definitions
Lemmas
list
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
pos
length
2
1.
A
: Type
2.
A
List
3.
u
:
A
4.
v
:
A
List
u
.
v
= nil
||
u
.
v
||
1
By:
AbReduce 0 THEN Analyze 0
Generated subgoal:
1
5.
u
.
v
= nil
||
v
||+1
1
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(4steps total)
PrintForm
Definitions
Lemmas
list
1
Sections
StandardLIB
Doc
u.v = nil 
||u.v||
1 u.v = nil ||u.v||1u.v = nil
||v||+11
