(13steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc
At:
list
length
wf
nat
1
1
1
1
2
2
1.
T:
Type
2.
L:
T List
3.
u:
T
4.
v:
T List
5.
(Case of v; nil
0 ; h.t
1+Y((
l,L. Case of L; nil
0 ; h.t
1+l(t)),t))
0
1+(Case of v; nil
0 ; h.t
1+Y((
l,L. Case of L; nil
0 ; h.t
1+l(t)),t))
By:
GenConcl ((Case of v; nil
0 ; h.t
1+Y((
l,L. Case of L; nil
0 ; h.t
1+l(t)),t)) = n)
Generated subgoal:
1
6.
n:
7.
(Case of v; nil
0 ; h.t
1+Y((
l,L. Case of L; nil
0 ; h.t
1+l(t)),t)) = n
0
1+n
About:
(13steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc