Thm*  k1,k2: .  f:((k1+k2)  (k1+k2)). Inj(k1+k2; (k1+k2); f) | [union_cardinality1] |
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)) (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* s:T List. no_repeats(T;s) (f:(||s||T). Inj(||s||; T; f)) | [no_repeats_inj] |
| 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* a,c,b,d:T List. (a @ b) = (c @ d) (e:T List. a = (c @ e) & d = (e @ b)  c = (a @ e) & b = (e @ d)) | [equal_appends] |
| 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* 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: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* f:(AB). Bij(A; B; f) (g:(BA). Bij(B; A; g) & InvFuns(A; B; f; g)) | [inverse-biject] |
Thm* x1,z,x2,x3:T List. ||z|| ||x1|| (x1 @ x2) = (z @ x3) (z':T List. x1 = (z @ z') & x3 = (z' @ x2)) | [equal_appends_case2] |
| Thm* x1,z,x2,x3:T List. ||x1||||z|| (x1 @ x2) = (z @ x3) (z':T List. z = (x1 @ z') & x2 = (z' @ x3)) | [equal_appends_case1] |
Thm* L:T List, P:(T ). (xL.P(x)) (i:||L||. P(L[i])) | [assert_l_bexists] |
B(x)