is mentioned by

Thm* (x,y:T. Dec(x = y)) (L,M:T List. Dec(L = M))	[decidable__equal_list]
Thm* eq:{T}, L,M:T List. Dec(L(~eq)M)	[decidable__list_iso]
Thm* eq:{T}, L,M:T List. Dec(L(eq)M)	[decidable__sublist]
Thm* eq:(TT), L1,L2:T List. Dec(disjoint(eq;L1;L2))	[decidable__disjoint]
Thm* P:(TProp). (x:T. Dec(P(x))) (L:T List. xL.(P(x)) xL.P(x))	[not_list_all_not_iff_list_exists]
Thm* P:(TProp), L:T List. (x:T. Dec(P(x))) Dec(xL.P(x))	[decidable__list_exists]
Thm* P:(TProp), L:T List. (x:T. Dec(P(x))) Dec(xL.P(x))	[decidable__list_all]
Thm* eq:(TT), x:T, L:T List. Dec(x(eq) L)	[decidable__is_member]

In prior sections: core int 1 bool 1 core 3 jlc int 2 discrete jlc