(3steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc
At:
list
length
non
negative
T:Type, L:T List. |
|(L)
0
By:
UnivCD
THEN
ListInd 2
THEN
AbReduce 0
Generated subgoals:
1
1.
T:
Type
2.
L:
T List
0
0
2
1.
T:
Type
2.
L:
T List
3.
u:
T
4.
v:
T List
5.
|
|(v)
0
1+|
|(v)
0
About:
(3steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc