is mentioned by

Thm* n:, P:((n+1)Prop). (x:(n+1). P(x)) P(0) & (x:n. P(x+1))	[all-nsub-add1]
Thm* L:(A+B) List, a:A. mapoutl(L) = [a] (L1,L2:(A+B) List. L = (L1 @ [inl(a)] @ L2) & mapoutl(L1) = nil & mapoutl(L2) = nil)	[mapoutl_is_singleton]
Thm* L:(A+B) List, l1,l2:A List. mapoutl(L) = (l1 @ l2) (L1,L2:(A+B) List. L = (L1 @ L2) & mapoutl(L1) = l1 & mapoutl(L2) = l2)	[mapoutl_is_append]
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* L:T List. no_repeats(T;rev(L)) no_repeats(T;L)	[no_repeats_reverse]
Thm* l1,l2:T List. no_repeats(T;l1 @ l2) l_disjoint(T;l1;l2) & no_repeats(T;l1) & no_repeats(T;l2)	[no_repeats_append_iff]
Thm* a,b,c:T List. l_disjoint(T;c;a @ b) l_disjoint(T;c;a) & l_disjoint(T;c;b)	[l_disjoint_append2]
Thm* a,b,c:T List. l_disjoint(T;a @ b;c) l_disjoint(T;a;c) & l_disjoint(T;b;c)	[l_disjoint_append]
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* L:T List, x,y:T. x before y L (L1,L2,L3:T List. L = (L1 @ [x] @ L2 @ [y] @ L3))	[l_before-iff]
Thm* x:T, L:T List. (x rev(L)) (x L)	[member_reverse]
Thm* R:(AA'Prop), P:(BA), P':(BA'), F,G,H:(BAA), F',G',H':(BA'A'), N:(BA(B List)), N':(BA'(B List)), M:(A), M':(A'). (i:B, s:A. P(i,s) M(F(i,s))M(s)) (i:B, s:A. M(G(i,s))M(s)) (i:B, s:A. P(i,s) M(H(i,s)) < M(s)) (i:B, s:A'. P'(i,s) M'(F'(i,s))M'(s)) (i:B, s:A'. M'(G'(i,s))M'(s)) (i:B, s:A'. P'(i,s) M'(H'(i,s)) < M'(s)) (j:B, u:A, v:A'. R(u,v) (P(j,u) P'(j,v))) (j:B, u:A, v:A'. R(u,v) P(j,u) P'(j,v) R(F(j,u),F'(j,v))) (j:B, u:A, v:A'. R(u,v) P(j,u) P'(j,v) R(H(j,u),H'(j,v))) (j:B, u:A, v:A'. R(u,v) R(G(j,u),G'(j,v))) (j:B, u:A, v:A'. R(u,v) N(j,u) = N'(j,v)) (j:B, u:A, v:A'. R(u,v) R(process u j where process s i == if P(i,s) then F(i,s) else G(i,s) where xs := N(i,s); s:= H(i,s); while not null xs { s := process s (hd xs); xs := tl xs; } ,process v j where process s i == if P'(i,s) then F'(i,s) else G'(i,s) where xs := N'(i,s); s:= H'(i,s); while not null xs { s := process s (hd xs); xs := tl xs; } ))	[accumulate-rel]
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* C,A,B:T List. C A @ B (A',B':T List. C = (A' @ B') & A' A & B' B)	[sublist_append_iff]
Thm* x,y,z:T List. (x @ z) = (y @ z) x = y	[equal_append_front]
Thm* l1,l2:T List. nil = (l1 @ l2) l1 = nil & l2 = nil	[nil_is_append]
Thm* i,j,k:. (k upto(i;j)) ik & k < j	[member_upto]
Thm* L:T List, P:(T). (xL.P(x)) (i:||L||. P(L[i]))	[assert_l_bexists]
Thm* L:T List, P:(T). (xL.P(x)) (i:||L||. P(L[i]))	[assert_l_ball]

In prior sections: core fun 1 well fnd int 1 bool 1 int 2 list 1 rel 1 mb basic mb nat mb list 1 num thy 1 mb list 2

Try larger context: Graphs