Nuprl - Pf discrete list 1 1

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

y:T List. Dec(x = y)

By: ListInd 3

Generated subgoals:

1 y:T List. Dec(nil = y)

2 4. u: T
5. v: T List
6. y:T List. Dec(v = y)
y:T List. Dec(u.v = y)

About:

1	`y:T List. Dec(nil = y)`
2	4. `u:` `T` 5. `v:` `T List` 6. `y:T List. Dec(v = y)` `y:T List. Dec(u.v = y)`