(11steps 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:
list
decomp
reverse
T
:Type,
L
:
T
List. 0<||
L
||
(
x
:
T
,
L'
:
T
List.
L
= (
L'
@ [
x
]))
By:
UnivCD
Generated subgoal:
1
1.
T
: Type
2.
L
:
T
List
3. 0<||
L
||
x
:
T
,
L'
:
T
List.
L
= (
L'
@ [
x
])
10
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(11steps total)
PrintForm
Definitions
mb
list
1
Sections
MarkB
generic
Doc
T:Type, L:T List. 0<||L|| 
(
x:T, L':T List. L = (L' @ [x]))
