is mentioned by

Thm* eq:{T=}, x,y:T, L:T List. x(eq) L eq(x,y) x(eq) remove(eq;y;L)	[not_is_member_remove_lemma]
Thm* eq:{T=}, L,M:T List. disjoint(eq;L;M) (x:T. x(eq) L & x(eq) M)	[not_disjoint_is_member_lemma]
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* eq:{T}, P:(T), L:T List. xL.P(x) (x:{x:T| x(eq) L }. P(x))	[not_list_all_2_implies_exists_not]

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