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

At: discrete list 1 1 1 1 2 1 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

0 = 1+||(v) False
By: GenConcl (||(v) = n)
Generated subgoals:

None

About:
listconsnilnatural_numberaddapplyuniverseequalimpliesfalse

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