PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: firstn lem1 1 1 1
1. T: Type
2. as: T*

0 < ||nil|| (Case of nil; nil nil ; a.as' a.firstn(0;as')) = ((Case of nil; nil nil ; a.as' nil) @ [nil[0]]) T*
By: Reduce 0
Generated subgoals:

None

About:
impliesless_thannatural_numbernilequal
listlist_indconsuniverse