PrintForm
Definitions
Lemmas
mb
list
1
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
last
cons
T
:Type,
L
:
T
List,
x
:
T
.
null(
L
)
last([
x
/
L
]) = last(
L
)
By:
Unfold `last` 0 THEN Reduce 0 THEN Assert (||
L
||>0)
THENL
[RW assert_pushdownC -1 THEN Easy
;RWO
Thm*
a
:
T
,
as
:
T
List,
i
:
. 0<
i
i
||
as
||
[
a
/
as
][
i
] =
as
[(
i
-1)] 0]
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
Lemmas
mb
list
1
Sections
MarkB
generic
Doc