Nuprl - Pf discrete list 1 1 1

(44steps) PrintForm Definitions Lemmas list 3 jlc Sections Support(jlc) Doc

At: discrete list 1 1 1

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

y:T List. Dec(nil = y)

By: Analyze 0 THEN UnfoldTopAb 0

Generated subgoal:

1 4. y: T List
nil = y nil = y

About:

(44steps) PrintForm Definitions Lemmas list 3 jlc Sections Support(jlc) Doc