At: lang sing prod 1 1 1 1 1 1 2
1. Alph: Type
2. L: Alph*
Prop
3. l: Alph*
4. i: {0...||l||}
5. (l[0..i
]) = nil
6. L(l[i..||l||])
7. ||l[0..i]|| = ||nil|| 
L(l)
By: RWH
(LemmaC
Thm* 
as:T*, i:{0...||as||}, j:{i...||as||}. ||as[i..j]|| = j-i)
7
Generated subgoal:| 1 | 7. i-0 = ||nil||
L(l) |
About:
