At: lang prod sing 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(l[0..||l||
])
6. (l[i..||l||]) = nil
7. ||l||-i = 0
8. ||l|| = i
L(l)
By: RWH
(LemmaC
Thm* 
as:T*. (as[0..||as||]) = as)
5
Generated subgoals:None
About:
