At: auto2 list ind 1 1 1 2 1 1 1 1
1. Alph: Type
2. P: Alph*
Prop
3. n: 
4. 0 < n
5. (
l:Alph*. ||l|| < n-1 
P(l)) (l:Alph*. ||l|| = n-1 P(l))
6. l: Alph*
7. ||l|| < n
8. ||l|| < n-1
9. ||l|| < n-1 P(l)
P(l)
By: ProveProp
Generated subgoals:None
About:
