Nuprl - Pf tl_append

PrintForm Definitions nfa 1 Sections AutomataTheory Doc

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

tl((l @ m)) = (tl(l) @ m)

By: ListInd 2

Generated subgoals:

1 ||nil|| > 0 tl((nil @ m)) = (tl(nil) @ m)

2 4. u: T
5. v: T*
6. ||v|| > 0 tl((v @ m)) = (tl(v) @ m)
||u.v|| > 0 tl(((u.v) @ m)) = (tl((u.v)) @ m)

About:

1	`\|\|nil\|\| > 0 tl((nil @ m)) = (tl(nil) @ m)`
2	4. `u:` `T` 5. `v:` `T*` 6. `\|\|v\|\| > 0 tl((v @ m)) = (tl(v) @ m)` `\|\|u.v\|\| > 0 tl(((u.v) @ m)) = (tl((u.v)) @ m)`