is mentioned by

Thm* s:(A+B) List, x:A. (x mapoutl(s)) (inl(x) s)	[mapoutl_member]
Thm* s:(A+B) List, x:A. (x mapoutl(s)) (y:A+B. (y s) & isl(y) & x = outl(y))	[member_mapoutl]
Thm* A,B:T List. no_repeats(T;A) (x:T. (x A) (x B)) (x:T. (x A) & (x B)) ||A|| < ||B||	[length_less]
Thm* A,B:T List. no_repeats(T;A) (x:T. (x A) (x B)) ||A||||B||	[length_le]
Thm* a,b:T List, t:T. l_disjoint(T;b;[t / a]) (t b) & l_disjoint(T;b;a)	[l_disjoint_cons2]
Thm* a,b:T List, t:T. l_disjoint(T;[t / a];b) (t b) & l_disjoint(T;a;b)	[l_disjoint_cons]
Thm* x:T, L:T List. (x rev(L)) (x L)	[member_reverse]
Thm* L:T List, x,y:T. x before y L (A,B:T List. L = (A @ B) & (x A) & (y B))	[l_before_decomp]
Thm* A,B:T List, x,y:T. x before y A @ B x before y A x before y B (x A) & (y B)	[l_before_append_iff]
Thm* (x,y:T. Dec(x = y)) (s:T List, z:T. (z s) (s1,s2:T List. s = (s1 @ [z / s2]) & (z s1)))	[l_member_decomp2]
Thm* s:T List, z:T. (z s) (s1,s2:T List. s = (s1 @ [z / s2]))	[l_member_decomp]
Thm* i,j,k:. (k upto(i;j)) ik & k < j	[member_upto]

In prior sections: mb list 1 mb list 2

Try larger context: Graphs