(2steps 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:
append
nil
sq
T
:Type,
l
:
T
List. (
l
@ nil) ~
l
By:
UnivCD THEN ListInd -1 THEN Reduce 0 THEN Try (Complete Auto)
Generated subgoal:
1
1.
T
: Type
2.
T
List
3.
u
:
T
4.
v
:
T
List
5. (
v
@ nil) ~
v
[
u
/ (
v
@ nil)] ~ [
u
/
v
]
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
mb
list
1
Sections
MarkB
generic
Doc
T:Type, l:T List. (l @ nil) ~ l T:Type, l:T List. (l @ nil) ~ l [u / (v @ nil)] ~ [u / v]
