PrintForm Definitions nfa 1 Sections AutomataTheory Doc

At: tl append front


T:Type, l,m:T*. ||l|| > 0 tl((l @ m)) = (tl(l) @ m)

By: UnivCD

Generated subgoal:

11. T: Type
2. l: T*
3. m: T*
4. ||l|| > 0
tl((l @ m)) = (tl(l) @ m)


About:
alluniverselistimpliesnatural_numberequal