At: nth tl lem0 2 1 1
1. T: Type
2. y: 
3. 0 < y
4. 
as:T*. tl(nth_tl(y-1;as)) = nth_tl(y-1+1;as)
5. 0 < y
6. as: T*
7. tl(nth_tl(y-1;tl(as))) = nth_tl(y-1+1;tl(as))
8. 0 < y+1
tl(nth_tl(y-1;tl(as))) = nth_tl(y+1-1;tl(as))
By: RWH (HypC -2) 0
Generated subgoals:None
About:
