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