(18steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
At:
list
all
iff
assert
list
all
2
2
1.
T:
Type
2.
L:
T List
3.
P:
T
4.
x
L.P(x)
x
L.P(x)
By:
MoveToConcl 4
THEN
ListInd 2
Generated subgoals:
1
x
nil.P(x)
x
nil.P(x)
2
4.
u:
T
5.
v:
T List
6.
x
v.P(x)
x
v.P(x)
x
(u.v).P(x)
x
(u.v).P(x)
About:
(18steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc