(7steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

At: assert l ball
T:Type, L:T List, P:(T). (xL.P(x)) (i:||L||. P(L[i]))
By:
InductionOnList
THEN
Reduce 0
THEN
Try (RW assert_pushdownC 0)
Generated subgoals:

11. T: Type
2. L: T List
3. u: T
4. v: T List
5. P:(T). (xv.P(x)) (i:||v||. P(v[i]))
6. P: T
7. P(u)
8. (xv.P(x))
9. i: (||v||+1)
P([u / v][i])		2 steps
 
21. T: Type
2. L: T List
3. u: T
4. v: T List
5. P:(T). (xv.P(x)) (i:||v||. P(v[i]))
6. P: T
7. i:(||v||+1). P([u / v][i])
P(u)		1 step
 
31. T: Type
2. L: T List
3. u: T
4. v: T List
5. P:(T). (xv.P(x)) (i:||v||. P(v[i]))
6. P: T
7. i:(||v||+1). P([u / v][i])
(xv.P(x))		3 steps

About:
listconsboolassertnatural_numberfunctionuniverseall

(7steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc