Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

T:. x,y:. as:T List. nth_tl(x;nth_tl(y;as)) = nth_tl(x + y;as)

Applied Tactic: (D 0 THENM D 0 ...a)
Generated subgoals:

1. y:. as:T List. nth_tl(x;nth_tl(y;as)) = nth_tl(x + y;as)