Level: Lib Thy Top:
Hypotheses:None
Conclusion:
T:
. y:
. as:T List. tl(nth_tl(y;as)) = nth_tl(y + 1;as)
Applied Tactic: (D 0 THENM D 0 THENM NatInd 2 ...a)
Generated subgoals:1. as:T List. tl(nth_tl(0;as)) = nth_tl(0 + 1;as)2. as:T List. tl(nth_tl(y;as)) = nth_tl(y + 1;as)