PrintForm Definitions nfa 1 Sections AutomataTheory Doc

At: hd append back 1 1

1. T: Type
2. l: T*
3. m: T*
4. ||m|| > 0

||nil|| = 0 hd((nil @ m)) = hd(m)

By: Reduce 0

Generated subgoals:

None


About:
impliesequalintnilnatural_numberuniverselist