Nuprl - Pf append nil right identity 1

1. T: Type
2. L: T List

(L @ nil) = L

By: ListInd -1 THEN Reduce 0

Generated subgoals:

1 nil = nil T List

2 3. u: T
4. v: T List
5. (v @ nil) = v
u.(v @ nil) = u.v

About:

1	`nil = nil T List`
2	3. `u:` `T` 4. `v:` `T List` 5. `(v @ nil) = v` `u.(v @ nil) = u.v`