mb
list
1
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
l
:
T
List,
x
:
T
. no_repeats(
T
;[
x
/
l
])
no_repeats(
T
;
l
) &
(
x
l
)
[no_repeats_cons]
cites the following:
Thm*
a
:
T
,
as
:
T
List,
i
:
. 0<
i
i
||
as
||
[
a
/
as
][
i
] =
as
[(
i
-1)]
[select_cons_tl]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb
list
1
Sections
MarkB
generic
Doc