Nuprl - Pf hd_reverse 1 2

1. T: Type
2. l: T*
3. u: T
4. v: T*
5. ||v|| > 0 hd(rev(v)) = v[(||v||-1)]

||u.v|| > 0 hd(rev(u.v)) = (u.v)[(||u.v||-1)]

By: Decide (||v|| = 0)

Generated subgoals:

1 6. ||v|| = 0
||u.v|| > 0 hd(rev(u.v)) = (u.v)[(||u.v||-1)]

2 6. ||v|| = 0
||u.v|| > 0 hd(rev(u.v)) = (u.v)[(||u.v||-1)]

About:

1	6. `\|\|v\|\| = 0` `\|\|u.v\|\| > 0 hd(rev(u.v)) = (u.v)[(\|\|u.v\|\|-1)]`
2	6. `\|\|v\|\| = 0` `\|\|u.v\|\| > 0 hd(rev(u.v)) = (u.v)[(\|\|u.v\|\|-1)]`