(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:
reverse
append
1
1.
T
: Type
2.
T
List
bs
:
T
List. rev(
bs
) = (rev(
bs
) @ nil)
By:
RWO
Thm*
as
:
T
List. (
as
@ nil) =
as
0
Generated subgoals:
None
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
bs:T List. rev(bs) = (rev(bs) @ nil) bs:T List. rev(bs) = (rev(bs) @ nil)as:T List. (as @ nil) = as 0
