list
3
jlc
Sections
Support(jlc)
Doc
Rank
Theorem
Name
2
Thm*
(
x,y:T. Dec(x = y))
(
L,M:T List. Dec(L = M))
[decidable__equal_list]
cites
1
Thm*
Discrete{T}
Discrete{(T List)}
[discrete__list]
list
3
jlc
Sections
Support(jlc)
Doc
x,y:T. Dec(x = y)) 
(L,M:T List. Dec(L = M)) Discrete{(T List)}x,y:T. Dec(x = y)) (L,M:T List. Dec(L = M)) Discrete{(T List)}