PrintForm Definitions nfa 1 Sections AutomataTheory Doc

At: length reverse 1

1. T: Type
2. l: T*

||rev(l)|| = ||l||

By: ListInd 2

Generated subgoals:

1 ||rev(nil)|| = ||nil||
23. u: T
4. v: T*
5. ||rev(v)|| = ||v||
||rev(u.v)|| = ||u.v||


About:
equalintuniverselistnilcons