Nuprl - Pf discrete list 1 1 1 1

At: discrete list 1 1 1 1

1. T: Type
2. Discrete{T}
3. x: T List
4. y: T List

nil = y nil = y

By: Analyze 4

Generated subgoals:

1 nil = nil T List nil = nil T List

2 5. u: T
6. v: T List
nil = u.v nil = u.v

About:

1	`nil = nil T List nil = nil T List`
2	5. `u:` `T` 6. `v:` `T List` `nil = u.v nil = u.v`