PrintForm Definitions nfa 1 Sections AutomataTheory Doc

At: hd map


A,B:Type, l:A*, f:(AB). ||l|| > 0 hd(map(f;l)) = f(hd(l))

By: UnivCD

Generated subgoal:

11. A: Type
2. B: Type
3. l: A*
4. f: AB
5. ||l|| > 0
hd(map(f;l)) = f(hd(l))


About:
alluniverselistfunctionimpliesnatural_numberequalapply