Nuprl - Pf nth_tl

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*

tl(nth_tl(y-1;tl(as))) = nth_tl(y+1;as)

By: InstHyp [tl(as)] 4 THEN RWH (AddrC [3] (RecUnfoldC `nth_tl`)) 0 THEN SplitOnConclITE

Generated subgoal:

1 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))

About: