(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
A
:Type,
l
:
A
List.
l
= nil
||
l
||
1
By:
(RepeatMFor 2 (Analyze 0)) THEN (Analyze 2)
Generated subgoals:
1
1.
A
: Type
2.
A
List
nil = nil
A
List
||nil||
1
1
step
2
1.
A
: Type
2.
A
List
3.
u
:
A
4.
v
:
A
List
u
.
v
= nil
||
u
.
v
||
1
2
steps
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
A:Type, l:A List. 
l = nil 
||l||
1 A:Type, l:A List. l = nil ||l||1 nil = nil 
A List ||nil||1
u.v = nil ||u.v||1
