PrintForm Definitions nfa 1 Sections AutomataTheory Doc

At: hd append front

T:Type, l,m:T*. ||l|| > 0 hd((l @ m)) = hd(l)
By: UnivCD
Generated subgoal:

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

About:
alluniverselistimpliesnatural_numberequal