Nuprl - Pf discrete list 1 1 1 1 2

At: discrete list 1 1 1 1 2

1. T: Type
2. Discrete{T}
3. x: T List
4. y: T List
5. u: T
6. v: T List

nil = u.v nil = u.v

By: DNth 2 0 THEN Analyze 0

Generated subgoal:

1 7. nil = u.v
False

About: