Nuprl - Pf discrete list 1 1 1 1 2 1

At: discrete list 1 1 1 1 2 1

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

False

By: ApFunToHypEquands `L' (||(L)) -1 THEN Reduce -1 THEN MoveToConcl -1

Generated subgoal:

1 0 = 1+||(v) False

About: