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

At: decidable equal list

T:Type. (x,y:T. Dec(x = y)) (L,M:T List. Dec(L = M))
By:
Fold `discrete` 0
THEN
UnivCD
Generated subgoal:

11. T: Type
2. Discrete{T}
Discrete{(T List)}

About:
listdecidableuniverseequalimpliesall

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