PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: nth tl lem1 1 1
1. T: Type

y:, as:T*. nth_tl(0;nth_tl(y;as)) = nth_tl(0+y;as)
By:
ArithSimp 0
THEN
RecUnfold `nth_tl` 0
THEN
Reduce 0
Generated subgoals:

None

About:
alllistequalnatural_numberadduniverse