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

At: discrete list 1
1. T: Type
2. Discrete{T}

Discrete{(T List)}
By: Analyze 0
Generated subgoal:

13. x: T List
y:T List. Dec(x = y)

About:
listdecidableuniverseequalall

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