1	# bend-mathlib/list.bend: List lemmas (append, reverse, length, take, drop, map, fold, filter).
2	import Base
3	import ./nat.bend as MNat
4	import ./bool.bend as MBool
5	
6	# The empty list is a right identity for append: xs ++ [] = xs.
7	law append_nil:
8	  for -a: Quant
9	  for -A: Kind(a)
10	  for xs: List<a, A>
11	  {List.append(a, A, xs, Nil{}) == xs : List<a, A>}
12	
13	def append_nil(a, A, xs):
14	  match xs:
15	    case Nil{}:
16	      {==}
17	    case h <> t:
18	      %append_nil(a, A, t) : {h <> List.append(a, A, t, Nil{}) == h <> _ : List<a, A>}
19	      {==}
20	
21	# The empty list is a left identity for append: [] ++ xs = xs.
22	law nil_append:
23	  for -a: Quant
24	  for -A: Kind(a)
25	  for -xs: List<a, A>
26	  {List.append(a, A, Nil{}, xs) == xs : List<a, A>}
27	
28	def nil_append(a, A, xs):
29	  {==}
30	
31	# Append is associative: (xs ++ ys) ++ zs = xs ++ (ys ++ zs).
32	law append_assoc:
33	  for -a: Quant
34	  for -A: Kind(a)
35	  for xs: List<a, A>
36	  for -ys: List<a, A>
37	  for -zs: List<a, A>
38	  {List.append(a, A, List.append(a, A, xs, ys), zs) == List.append(a, A, xs, List.append(a, A, ys, zs)) : List<a, A>}
39	
40	def append_assoc(a, A, xs, ys, zs):
41	  match xs:
42	    case Nil{}:
43	      {==}
44	    case h <> t:
45	      %append_assoc(a, A, t, ys, zs) : {h <> List.append(a, A, List.append(a, A, t, ys), zs) == h <> _ : List<a, A>}
46	      {==}
47	
48	# The length of an append is the sum of the lengths.
49	law length_append:
50	  for -a: Quant
51	  for -A: Kind(a)
52	  for xs: List<a, A>
53	  for -ys: List<a, A>
54	  {List.length(a, A, List.append(a, A, xs, ys)) == Nat.add(List.length(a, A, xs), List.length(a, A, ys)) : Nat}
55	
56	def length_append(a, A, xs, ys):
57	  match xs:
58	    case Nil{}:
59	      {==}
60	    case h <> t:
61	      %length_append(a, A, t, ys) : {1n+List.length(a, A, List.append(a, A, t, ys)) == 1n+_ : Nat}
62	      {==}
63	
64	def internal_reverse_go_append(a, -A: Kind(a), xs: List<a, A>, -ys: List<a, A>, -acc: List<a, A>) -> {List.reverse.go(a, A, xs, List.append(a, A, ys, acc)) == List.append(a, A, List.reverse.go(a, A, xs, ys), acc) : List<a, A>}:
65	  match xs:
66	    case Nil{}:
67	      {==}
68	    case h <> t:
69	      internal_reverse_go_append(a, A, t, h <> ys, acc)
70	
71	# The reverse accumulator loop appends the reversed list to the accumulator.
72	law reverse_go_spec:
73	  for -a: Quant
74	  for -A: Kind(a)
75	  for xs: List<a, A>
76	  for -acc: List<a, A>
77	  {List.reverse.go(a, A, xs, acc) == List.append(a, A, List.reverse(a, A, xs), acc) : List<a, A>}
78	
79	def reverse_go_spec(a, A, xs, acc):
80	  match xs:
81	    case Nil{}:
82	      {==}
83	    case h <> t:
84	      internal_reverse_go_append(a, A, t, h <> Nil{}, acc)
85	
86	def internal_reverse_append_go(a, -A: Kind(a), xs: List<a, A>, -ys: List<a, A>, -acc: List<a, A>) -> {List.reverse.go(a, A, List.append(a, A, xs, ys), acc) == List.reverse.go(a, A, ys, List.reverse.go(a, A, xs, acc)) : List<a, A>}:
87	  match xs:
88	    case Nil{}:
89	      {==}
90	    case h <> t:
91	      internal_reverse_append_go(a, A, t, ys, h <> acc)
92	
93	# Reversing an append reverses and swaps the parts: reverse (xs ++ ys) = reverse ys ++ reverse xs.
94	law reverse_append:
95	  for -a: Quant
96	  for -A: Kind(a)
97	  for xs: List<a, A>
98	  for ys: List<a, A>
99	  {List.reverse(a, A, List.append(a, A, xs, ys)) == List.append(a, A, List.reverse(a, A, ys), List.reverse(a, A, xs)) : List<a, A>}
100	
101	def reverse_append(a, A, xs, ys):
102	  Equal.trans(List<a, A>, List.reverse(a, A, List.append(a, A, xs, ys)), List.reverse.go(a, A, ys, List.reverse(a, A, xs)), List.append(a, A, List.reverse(a, A, ys), List.reverse(a, A, xs)), internal_reverse_append_go(a, A, xs, ys, Nil{}), reverse_go_spec(a, A, ys, List.reverse(a, A, xs)))
103	
104	def internal_reverse_go_go(a, -A: Kind(a), xs: List<a, A>, -acc: List<a, A>) -> {List.reverse.go(a, A, List.reverse.go(a, A, xs, acc), Nil{}) == List.reverse.go(a, A, acc, xs) : List<a, A>}:
105	  match xs:
106	    case Nil{}:
107	      {==}
108	    case h <> t:
109	      internal_reverse_go_go(a, A, t, h <> acc)
110	
111	# Reversing twice gives the list back.
112	law reverse_reverse:
113	  for -a: Quant
114	  for -A: Kind(a)
115	  for xs: List<a, A>
116	  {List.reverse(a, A, List.reverse(a, A, xs)) == xs : List<a, A>}
117	
118	def reverse_reverse(a, A, xs):
119	  internal_reverse_go_go(a, A, xs, Nil{})
120	
121	def internal_length_reverse_go(a, -A: Kind(a), xs: List<a, A>, -acc: List<a, A>, +n: Nat, e: {List.length(a, A, acc) == n : Nat}) -> {List.length(a, A, List.reverse.go(a, A, xs, acc)) == Nat.add(n, List.length(a, A, xs)) : Nat}:
122	  match xs:
123	    case Nil{}:
124	      %Equal.sym(Nat, Nat.add(n, 0n), n, MNat.add_zero(n)) : {List.length(a, A, acc) == _ : Nat}
125	      e
126	    case h <> t:
127	      %Equal.sym(Nat, Nat.add(n, 1n+List.length(a, A, t)), 1n+Nat.add(n, List.length(a, A, t)), MNat.add_succ(n, List.length(a, A, t))) : {List.length(a, A, List.reverse.go(a, A, t, h <> acc)) == _ : Nat}
128	      internal_length_reverse_go(a, A, t, h <> acc, 1n+n, Equal.cong(Nat, Nat, k => 1n+k, List.length(a, A, acc), n, e))
129	
130	# Reversing preserves the length.
131	law length_reverse:
132	  for -a: Quant
133	  for -A: Kind(a)
134	  for xs: List<a, A>
135	  {List.length(a, A, List.reverse(a, A, xs)) == List.length(a, A, xs) : Nat}
136	
137	def length_reverse(a, A, xs):
138	  internal_length_reverse_go(a, A, xs, Nil{}, 0n, {==})
139	
140	# A right fold over an append folds the first part onto the fold of the second.
141	law foldr_append:
142	  for ~a: Quant
143	  for ~A: Kind(a)
144	  for ~B: Type
145	  for ~f: A -> B -> B
146	  for xs: List<a, A>
147	  for -ys: List<a, A>
148	  for -z: B
149	  {List.foldr(~a, ~A, ~B, ~f, List.append(a, A, xs, ys), z) == List.foldr(~a, ~A, ~B, ~f, xs, List.foldr(~a, ~A, ~B, ~f, ys, z)) : B}
150	
151	def foldr_append(a, A, B, f, xs, ys, z):
152	  match xs:
153	    case Nil{}:
154	      {==}
155	    case h <> t:
156	      %foldr_append(~a, ~A, ~B, ~f, t, ys, z) : {f(h, List.foldr(~a, ~A, ~B, ~f, List.append(a, A, t, ys), z)) == f(h, _) : B}
157	      {==}
158	
159	# Taking n elements and appending the rest after dropping n gives the list back.
160	law take_append_drop:
161	  for -a: Quant
162	  for -A: Kind(a)
163	  for xs: List<a, A>
164	  for n: Nat
165	  {List.append(a, A, List.take(a, A, xs, n), List.drop(a, A, xs, n)) == xs : List<a, A>}
166	
167	def take_append_drop(a, A, xs, n):
168	  match xs n:
169	    case Nil{} _:
170	      {==}
171	    case h <> t 0n:
172	      {==}
173	    case h <> t 1n+p:
174	      %take_append_drop(a, A, t, p) : {h <> List.append(a, A, List.take(a, A, t, p), List.drop(a, A, t, p)) == h <> _ : List<a, A>}
175	      {==}
176	
177	# Mapping preserves the length.
178	law length_map:
179	  for ~A: Type
180	  for ~B: Type
181	  for ~f: A -> B
182	  for xs: List<A>
183	  {List.length(&1, B, List.map(~A, ~B, ~f, xs)) == List.length(&1, A, xs) : Nat}
184	
185	def length_map(A, B, f, xs):
186	  match xs:
187	    case Nil{}:
188	      {==}
189	    case h <> t:
190	      %length_map(~A, ~B, ~f, t) : {1n+List.length(&1, B, List.map(~A, ~B, ~f, t)) == 1n+_ : Nat}
191	      {==}
192	
193	# Mapping over an append maps each part: map f (xs ++ ys) = map f xs ++ map f ys.
194	law map_append:
195	  for ~A: Type
196	  for ~B: Type
197	  for ~f: A -> B
198	  for xs: List<A>
199	  for -ys: List<A>
200	  {List.map(~A, ~B, ~f, List.append(&1, A, xs, ys)) == List.append(&1, B, List.map(~A, ~B, ~f, xs), List.map(~A, ~B, ~f, ys)) : List<B>}
201	
202	def map_append(A, B, f, xs, ys):
203	  match xs:
204	    case Nil{}:
205	      {==}
206	    case h <> t:
207	      %map_append(~A, ~B, ~f, t, ys) : {f(h) <> List.map(~A, ~B, ~f, List.append(&1, A, t, ys)) == f(h) <> _ : List<B>}
208	      {==}
209	
210	# Mapping twice is mapping the composition: map g (map f xs) = map (g . f) xs.
211	law map_map:
212	  for ~A: Type
213	  for ~B: Type
214	  for ~C: Type
215	  for ~f: A -> B
216	  for ~g: B -> C
217	  for xs: List<A>
218	  {List.map(~B, ~C, ~g, List.map(~A, ~B, ~f, xs)) == List.map(~A, ~C, ~(x => g(f(x))), xs) : List<C>}
219	
220	def map_map(A, B, C, f, g, xs):
221	  match xs:
222	    case Nil{}:
223	      {==}
224	    case h <> t:
225	      %map_map(~A, ~B, ~C, ~f, ~g, t) : {g(f(h)) <> List.map(~B, ~C, ~g, List.map(~A, ~B, ~f, t)) == g(f(h)) <> _ : List<C>}
226	      {==}
227	
228	# Taking zero elements gives the empty list.
229	law take_zero:
230	  for -a: Quant
231	  for -A: Kind(a)
232	  for xs: List<a, A>
233	  {List.take(a, A, xs, 0n) == Nil{} : List<a, A>}
234	
235	def take_zero(a, A, xs):
236	  match xs:
237	    case Nil{}:
238	      {==}
239	    case h <> t:
240	      {==}
241	
242	# Dropping zero elements gives the list back.
243	law drop_zero:
244	  for -a: Quant
245	  for -A: Kind(a)
246	  for xs: List<a, A>
247	  {List.drop(a, A, xs, 0n) == xs : List<a, A>}
248	
249	def drop_zero(a, A, xs):
250	  match xs:
251	    case Nil{}:
252	      {==}
253	    case h <> t:
254	      {==}
255	
256	# Taking from the empty list gives the empty list.
257	law take_nil:
258	  for -a: Quant
259	  for -A: Kind(a)
260	  for -n: Nat
261	  {List.take(a, A, Nil{}, n) == Nil{} : List<a, A>}
262	
263	def take_nil(a, A, n):
264	  {==}
265	
266	# Dropping from the empty list gives the empty list.
267	law drop_nil:
268	  for -a: Quant
269	  for -A: Kind(a)
270	  for -n: Nat
271	  {List.drop(a, A, Nil{}, n) == Nil{} : List<a, A>}
272	
273	def drop_nil(a, A, n):
274	  {==}
275	
276	# Taking n elements leaves min(n, length) of them.
277	law length_take:
278	  for -a: Quant
279	  for -A: Kind(a)
280	  for xs: List<a, A>
281	  for n: Nat
282	  {List.length(a, A, List.take(a, A, xs, n)) == Nat.min(n, List.length(a, A, xs)) : Nat}
283	
284	def length_take(a, A, xs, n):
285	  match xs n:
286	    case Nil{} _:
287	      Equal.sym(Nat, Nat.min(n, 0n), 0n, MNat.min_zero(n))
288	    case h <> t 0n:
289	      {==}
290	    case h <> t 1n+p:
291	      %length_take(a, A, t, p) : {1n+List.length(a, A, List.take(a, A, t, p)) == 1n+_ : Nat}
292	      {==}
293	
294	# Dropping n elements leaves length - n of them.
295	law length_drop:
296	  for -a: Quant
297	  for -A: Kind(a)
298	  for xs: List<a, A>
299	  for n: Nat
300	  {List.length(a, A, List.drop(a, A, xs, n)) == Nat.sub(List.length(a, A, xs), n) : Nat}
301	
302	def length_drop(a, A, xs, n):
303	  match xs n:
304	    case Nil{} _:
305	      Equal.sym(Nat, Nat.sub(0n, n), 0n, MNat.zero_sub(n))
306	    case h <> t 0n:
307	      {==}
308	    case h <> t 1n+p:
309	      length_drop(a, A, t, p)
310	
311	# Taking as many elements as the list has gives the list back.
312	law take_length:
313	  for -A: Data
314	  for +xs: List<&2, A>
315	  {List.take(&2, A, xs, List.length(&2, A, xs)) == xs : List<&2, A>}
316	
317	def take_length(A, xs):
318	  match xs:
319	    case Nil{}:
320	      {==}
321	    case h <> t:
322	      %take_length(A, t) : {h <> List.take(&2, A, t, List.length(&2, A, t)) == h <> _ : List<&2, A>}
323	      {==}
324	
325	# Dropping as many elements as the list has gives the empty list.
326	law drop_length:
327	  for -A: Data
328	  for +xs: List<&2, A>
329	  {List.drop(&2, A, xs, List.length(&2, A, xs)) == Nil{} : List<&2, A>}
330	
331	def drop_length(A, xs):
332	  match xs:
333	    case Nil{}:
334	      {==}
335	    case h <> t:
336	      drop_length(A, t)
337	
338	# Taking m from the first n is taking min(n, m).
339	law take_take:
340	  for -a: Quant
341	  for -A: Kind(a)
342	  for xs: List<a, A>
343	  for n: Nat
344	  for m: Nat
345	  {List.take(a, A, List.take(a, A, xs, n), m) == List.take(a, A, xs, Nat.min(n, m)) : List<a, A>}
346	
347	def take_take(a, A, xs, n, m):
348	  match xs n m:
349	    case Nil{} _ _:
350	      {==}
351	    case h <> t 0n _:
352	      {==}
353	    case h <> t 1n+p 0n:
354	      {==}
355	    case h <> t 1n+p 1n+q:
356	      %take_take(a, A, t, p, q) : {h <> List.take(a, A, List.take(a, A, t, p), q) == h <> _ : List<a, A>}
357	      {==}
358	
359	# Dropping m after dropping n is dropping n + m.
360	law drop_drop:
361	  for -a: Quant
362	  for -A: Kind(a)
363	  for xs: List<a, A>
364	  for n: Nat
365	  for -m: Nat
366	  {List.drop(a, A, List.drop(a, A, xs, n), m) == List.drop(a, A, xs, Nat.add(n, m)) : List<a, A>}
367	
368	def drop_drop(a, A, xs, n, m):
369	  match xs n m:
370	    case Nil{} _ _:
371	      {==}
372	    case h <> t 0n _:
373	      {==}
374	    case h <> t 1n+p _:
375	      drop_drop(a, A, t, p, m)
376	
377	# Reversing the empty list gives the empty list.
378	law reverse_nil:
379	  for -a: Quant
380	  for -A: Kind(a)
381	  {List.reverse(a, A, Nil{}) == Nil{} : List<a, A>}
382	
383	def reverse_nil(a, A):
384	  {==}
385	
386	# Reversing a one-element list gives it back.
387	law reverse_singleton:
388	  for -a: Quant
389	  for -A: Kind(a)
390	  for -x: A
391	  {List.reverse(a, A, [x]) == [x] : List<a, A>}
392	
393	def reverse_singleton(a, A, x):
394	  {==}
395	
396	# Replicating x n times gives a list of length n.
397	law length_replicate:
398	  for -A: Data
399	  for n: Nat
400	  for -x: A
401	  {List.length(&2, A, List.replicate(A, n, x)) == n : Nat}
402	
403	def length_replicate(A, n, x):
404	  match n:
405	    case 0n:
406	      {==}
407	    case 1n+p:
408	      %length_replicate(A, p, x) : {1n+List.length(&2, A, List.replicate(A, p, x)) == 1n+_ : Nat}
409	      {==}
410	
411	# Range(n) has length n.
412	law length_range:
413	  for n: Nat
414	  {List.length(&2, Nat, List.range(n)) == n : Nat}
415	
416	def internal_length_range_go(+n: Nat, acc: List<&2, Nat>) -> {List.length(&2, Nat, List.range.go(n, acc)) == Nat.add(n, List.length(&2, Nat, acc)) : Nat}:
417	  match n:
418	    case 0n:
419	      {==}
420	    case 1n+p:
421	      %MNat.add_succ(p, List.length(&2, Nat, acc)) : {List.length(&2, Nat, List.range.go(p, p <> acc)) == _ : Nat}
422	      internal_length_range_go(p, p <> acc)
423	
424	def length_range(n):
425	  +n = n
426	  %Equal.sym(Nat, List.length(&2, Nat, List.range.go(n, Nil{})), Nat.add(n, 0n), internal_length_range_go(n, Nil{})) : {_ == n : Nat}
427	  MNat.add_zero(n)
428	
429	# Zipping two lists gives the length of the shorter one.
430	law length_zip:
431	  for -a: Quant
432	  for -A: Kind(a)
433	  for xs: List<a, A>
434	  for ys: List<a, A>
435	  {List.length(&1, A & A, List.zip(a, A, a, A, xs, ys)) == Nat.min(List.length(a, A, xs), List.length(a, A, ys)) : Nat}
436	
437	def length_zip(a, A, xs, ys):
438	  match xs ys:
439	    case Nil{} _:
440	      {==}
441	    case h <> t Nil{}:
442	      {==}
443	    case h <> t y <> yt:
444	      %length_zip(a, A, t, yt) : {1n+List.length(&1, A & A, List.zip(a, A, a, A, t, yt)) == 1n+_ : Nat}
445	      {==}
446	
447	# Appending after a cons: (x :: xs) ++ ys = x :: (xs ++ ys).
448	law append_cons:
449	  for -a: Quant
450	  for -A: Kind(a)
451	  for -x: A
452	  for -xs: List<a, A>
453	  for -ys: List<a, A>
454	  {List.append(a, A, x <> xs, ys) == x <> List.append(a, A, xs, ys) : List<a, A>}
455	
456	def append_cons(a, A, x, xs, ys):
457	  {==}
458	
459	# The empty list has length zero.
460	law length_nil:
461	  for -a: Quant
462	  for -A: Kind(a)
463	  {List.length(a, A, Nil{}) == 0n : Nat}
464	
465	def length_nil(a, A):
466	  {==}
467	
468	# A cons is one longer than its tail.
469	law length_cons:
470	  for -a: Quant
471	  for -A: Kind(a)
472	  for -x: A
473	  for -xs: List<a, A>
474	  {List.length(a, A, x <> xs) == 1n+List.length(a, A, xs) : Nat}
475	
476	def length_cons(a, A, x, xs):
477	  {==}
478	
479	# Concatenating an append concatenates each part: concat (xss ++ yss) = concat xss ++ concat yss.
480	law concat_append:
481	  for -a: Quant
482	  for -A: Kind(a)
483	  for xss: List<a, List<a, A>>
484	  for -yss: List<a, List<a, A>>
485	  {List.concat(a, A, List.append(a, List<a, A>, xss, yss)) == List.append(a, A, List.concat(a, A, xss), List.concat(a, A, yss)) : List<a, A>}
486	
487	def concat_append(a, A, xss, yss):
488	  match xss:
489	    case Nil{}:
490	      {==}
491	    case h <> t:
492	      %Equal.sym(List<a, A>, List.concat(a, A, List.append(a, List<a, A>, t, yss)), List.append(a, A, List.concat(a, A, t), List.concat(a, A, yss)), concat_append(a, A, t, yss)) : {List.append(a, A, h, _) == List.append(a, A, List.append(a, A, h, List.concat(a, A, t)), List.concat(a, A, yss)) : List<a, A>}
493	      Equal.sym(List<a, A>, List.append(a, A, List.append(a, A, h, List.concat(a, A, t)), List.concat(a, A, yss)), List.append(a, A, h, List.append(a, A, List.concat(a, A, t), List.concat(a, A, yss))), append_assoc(a, A, h, List.concat(a, A, t), List.concat(a, A, yss)))
494	
495	# A left fold over an append folds the second part from the fold of the first.
496	law foldl_append:
497	  for ~a: Quant
498	  for ~A: Kind(a)
499	  for ~B: Type
500	  for ~f: B -> A -> B
501	  for xs: List<a, A>
502	  for -ys: List<a, A>
503	  for -z: B
504	  {List.foldl(~a, ~A, ~B, ~f, List.append(a, A, xs, ys), z) == List.foldl(~a, ~A, ~B, ~f, ys, List.foldl(~a, ~A, ~B, ~f, xs, z)) : B}
505	
506	def foldl_append(a, A, B, f, xs, ys, z):
507	  match xs:
508	    case Nil{}:
509	      {==}
510	    case h <> t:
511	      foldl_append(~a, ~A, ~B, ~f, t, ys, f(z, h))
512	
513	# Mapping commutes with reversing: map f (reverse xs) = reverse (map f xs).
514	law map_reverse:
515	  for ~A: Type
516	  for ~B: Type
517	  for ~f: A -> B
518	  for xs: List<A>
519	  {List.map(~A, ~B, ~f, List.reverse(&1, A, xs)) == List.reverse(&1, B, List.map(~A, ~B, ~f, xs)) : List<B>}
520	
521	def internal_map_reverse_go(~A: Type, ~B: Type, ~f: A -> B, xs: List<A>, acc: List<A>) -> {List.map(~A, ~B, ~f, List.reverse.go(&1, A, xs, acc)) == List.reverse.go(&1, B, List.map(~A, ~B, ~f, xs), List.map(~A, ~B, ~f, acc)) : List<B>}:
522	  match xs:
523	    case Nil{}:
524	      {==}
525	    case h <> t:
526	      internal_map_reverse_go(~A, ~B, ~f, t, h <> acc)
527	
528	def map_reverse(A, B, f, xs):
529	  internal_map_reverse_go(~A, ~B, ~f, xs, Nil{})
530	
531	# All over an append is all over each part, joined by and.
532	law all_append:
533	  for ~a: Quant
534	  for ~A: Kind(a)
535	  for ~f: A -> Bool
536	  for xs: List<a, A>
537	  for -ys: List<a, A>
538	  {List.all(~a, ~A, ~f, List.append(a, A, xs, ys)) == Bool.and(List.all(~a, ~A, ~f, xs), List.all(~a, ~A, ~f, ys)) : Bool}
539	
540	def all_append(a, A, f, xs, ys):
541	  match xs:
542	    case Nil{}:
543	      {==}
544	    case h <> t:
545	      %Equal.sym(Bool, List.all(~a, ~A, ~f, List.append(a, A, t, ys)), Bool.and(List.all(~a, ~A, ~f, t), List.all(~a, ~A, ~f, ys)), all_append(~a, ~A, ~f, t, ys)) : {Bool.and(f(h), _) == Bool.and(Bool.and(f(h), List.all(~a, ~A, ~f, t)), List.all(~a, ~A, ~f, ys)) : Bool}
546	      Equal.sym(Bool, Bool.and(Bool.and(f(h), List.all(~a, ~A, ~f, t)), List.all(~a, ~A, ~f, ys)), Bool.and(f(h), Bool.and(List.all(~a, ~A, ~f, t), List.all(~a, ~A, ~f, ys))), MBool.and_assoc(f(h), List.all(~a, ~A, ~f, t), List.all(~a, ~A, ~f, ys)))
547	
548	# Any over an append is any over each part, joined by or.
549	law any_append:
550	  for ~a: Quant
551	  for ~A: Kind(a)
552	  for ~f: A -> Bool
553	  for xs: List<a, A>
554	  for -ys: List<a, A>
555	  {List.any(~a, ~A, ~f, List.append(a, A, xs, ys)) == Bool.or(List.any(~a, ~A, ~f, xs), List.any(~a, ~A, ~f, ys)) : Bool}
556	
557	def any_append(a, A, f, xs, ys):
558	  match xs:
559	    case Nil{}:
560	      {==}
561	    case h <> t:
562	      %Equal.sym(Bool, List.any(~a, ~A, ~f, List.append(a, A, t, ys)), Bool.or(List.any(~a, ~A, ~f, t), List.any(~a, ~A, ~f, ys)), any_append(~a, ~A, ~f, t, ys)) : {Bool.or(f(h), _) == Bool.or(Bool.or(f(h), List.any(~a, ~A, ~f, t)), List.any(~a, ~A, ~f, ys)) : Bool}
563	      Equal.sym(Bool, Bool.or(Bool.or(f(h), List.any(~a, ~A, ~f, t)), List.any(~a, ~A, ~f, ys)), Bool.or(f(h), Bool.or(List.any(~a, ~A, ~f, t), List.any(~a, ~A, ~f, ys))), MBool.or_assoc(f(h), List.any(~a, ~A, ~f, t), List.any(~a, ~A, ~f, ys)))
564	
565	# Filtering an append filters each part.
566	law filter_append:
567	  for ~A: Data
568	  for ~f: A -> Bool
569	  for xs: List<&2, A>
570	  for ys: List<&2, A>
571	  {List.filter(~A, ~f, List.append(&2, A, xs, ys)) == List.append(&2, A, List.filter(~A, ~f, xs), List.filter(~A, ~f, ys)) : List<&2, A>}
572	
573	def internal_filter_put_append(-A: Data, h: A, r: List<&2, A>, s: List<&2, A>, b: Bool) -> {List.append(&2, A, List.filter.put(A, h, r, b), s) == List.filter.put(A, h, List.append(&2, A, r, s), b) : List<&2, A>}:
574	  match b:
575	    case False{}:
576	      {==}
577	    case True{}:
578	      {==}
579	
580	def filter_append(A, f, xs, ys):
581	  match xs:
582	    case Nil{}:
583	      {==}
584	    case +h <> t:
585	      +ys = ys
586	      +t = t
587	      %Equal.sym(List<&2, A>, List.filter(~A, ~f, List.append(&2, A, t, ys)), List.append(&2, A, List.filter(~A, ~f, t), List.filter(~A, ~f, ys)), filter_append(~A, ~f, t, ys)) : {List.filter.put(A, h, _, f(h)) == List.append(&2, A, List.filter.put(A, h, List.filter(~A, ~f, t), f(h)), List.filter(~A, ~f, ys)) : List<&2, A>}
588	      Equal.sym(List<&2, A>, List.append(&2, A, List.filter.put(A, h, List.filter(~A, ~f, t), f(h)), List.filter(~A, ~f, ys)), List.filter.put(A, h, List.append(&2, A, List.filter(~A, ~f, t), List.filter(~A, ~f, ys)), f(h)), internal_filter_put_append(A, h, List.filter(~A, ~f, t), List.filter(~A, ~f, ys), f(h)))
589	
590	# An append contains x iff either part does.
591	law contains_append:
592	  for ~A: Data
593	  for ~eq: A -> A -> Bool
594	  for xs: List<&2, A>
595	  for -ys: List<&2, A>
596	  for +x: A
597	  {List.contains(~A, ~eq, List.append(&2, A, xs, ys), x) == Bool.or(List.contains(~A, ~eq, xs, x), List.contains(~A, ~eq, ys, x)) : Bool}
598	
599	def contains_append(A, eq, xs, ys, x):
600	  match xs:
601	    case Nil{}:
602	      {==}
603	    case h <> t:
604	      %Equal.sym(Bool, List.contains(~A, ~eq, List.append(&2, A, t, ys), x), Bool.or(List.contains(~A, ~eq, t, x), List.contains(~A, ~eq, ys, x)), contains_append(~A, ~eq, t, ys, x)) : {Bool.or(eq(h, x), _) == Bool.or(Bool.or(eq(h, x), List.contains(~A, ~eq, t, x)), List.contains(~A, ~eq, ys, x)) : Bool}
605	      Equal.sym(Bool, Bool.or(Bool.or(eq(h, x), List.contains(~A, ~eq, t, x)), List.contains(~A, ~eq, ys, x)), Bool.or(eq(h, x), Bool.or(List.contains(~A, ~eq, t, x), List.contains(~A, ~eq, ys, x))), MBool.or_assoc(eq(h, x), List.contains(~A, ~eq, t, x), List.contains(~A, ~eq, ys, x)))
606	
607	# Filtering never makes a list longer.
608	law length_filter_le:
609	  for ~A: Data
610	  for ~f: A -> Bool
611	  for xs: List<&2, A>
612	  {Nat.is_le(List.length(&2, A, List.filter(~A, ~f, xs)), List.length(&2, A, xs)) == True{} : Bool}
613	
614	def internal_length_filter_put_le(-A: Data, h: A, r: List<&2, A>, b: Bool) -> {Nat.is_le(List.length(&2, A, List.filter.put(A, h, r, b)), 1n+List.length(&2, A, r)) == True{} : Bool}:
615	  match b:
616	    case False{}:
617	      MNat.le_succ(List.length(&2, A, r))
618	    case True{}:
619	      MNat.le_refl(1n+List.length(&2, A, r))
620	
621	def length_filter_le(A, f, xs):
622	  match xs:
623	    case Nil{}:
624	      {==}
625	    case +h <> t:
626	      +t = t
627	      MNat.le_trans(List.length(&2, A, List.filter.put(A, h, List.filter(~A, ~f, t), f(h))), 1n+List.length(&2, A, List.filter(~A, ~f, t)), 1n+List.length(&2, A, t), internal_length_filter_put_le(A, h, List.filter(~A, ~f, t), f(h)), MNat.succ_le_succ(List.length(&2, A, List.filter(~A, ~f, t)), List.length(&2, A, t), length_filter_le(~A, ~f, t)))
628	
629	# Membership in a list, as a reusable proposition.
630	def mem(~A: Data, ~eq: A -> A -> Bool, +x: A, xs: List<&2, A>) -> Data:
631	  {List.contains(~A, ~eq, xs, x) == True{} : Bool}
632	
633	# A list is sorted by a comparator when every adjacent pair is in order.
634	def sorted_by(~A: Data, ~le: A -> A -> Bool, +xs: List<&2, A>) -> Data:
635	  {List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), List.zip(&2, A, &2, A, xs, List.tail(&2, A, xs))) == True{} : Bool}
636	
637	def internal_or_of_right(a: Bool, -b: Bool, hb: {b == True{} : Bool}) -> {Bool.or(a, b) == True{} : Bool}:
638	  match a:
639	    case False{}:
640	      hb
641	    case True{}:
642	      {==}
643	
644	def internal_or_of_or(a: Bool, -b: Bool, -c: Bool, h: {Bool.or(a, b) == True{} : Bool}, k: {b == True{} : Bool} -> {c == True{} : Bool}) -> {Bool.or(a, c) == True{} : Bool}:
645	  match a:
646	    case False{}:
647	      k(h)
648	    case True{}:
649	      {==}
650	
651	def internal_and_left(a: Bool, -b: Bool, h: {Bool.and(a, b) == True{} : Bool}) -> {a == True{} : Bool}:
652	  match a:
653	    case False{}:
654	      Empty.absurd({False{} == True{} : Bool}, MNat.internal_false_ne_true(h))
655	    case True{}:
656	      {==}
657	
658	def internal_and_right(a: Bool, -b: Bool, h: {Bool.and(a, b) == True{} : Bool}) -> {b == True{} : Bool}:
659	  match a:
660	    case False{}:
661	      Empty.absurd({b == True{} : Bool}, MNat.internal_false_ne_true(h))
662	    case True{}:
663	      h
664	
665	def internal_mem_append_left(+xs: List<&2, Nat>, +ys: List<&2, Nat>, +x: Nat, h: {List.contains(~Nat, ~Nat.is_eq, xs, x) == True{} : Bool}) -> {List.contains(~Nat, ~Nat.is_eq, List.append(&2, Nat, xs, ys), x) == True{} : Bool}:
666	  match xs:
667	    case Nil{}:
668	      Empty.absurd({List.contains(~Nat, ~Nat.is_eq, ys, x) == True{} : Bool}, MNat.internal_false_ne_true(h))
669	    case hd <> tl:
670	      internal_or_of_or(Nat.is_eq(hd, x), List.contains(~Nat, ~Nat.is_eq, tl, x), List.contains(~Nat, ~Nat.is_eq, List.append(&2, Nat, tl, ys), x), h, internal_mem_append_left(tl, ys, x))
671	
672	def internal_mem_append_right(+xs: List<&2, Nat>, +ys: List<&2, Nat>, +x: Nat, h: {List.contains(~Nat, ~Nat.is_eq, ys, x) == True{} : Bool}) -> {List.contains(~Nat, ~Nat.is_eq, List.append(&2, Nat, xs, ys), x) == True{} : Bool}:
673	  match xs:
674	    case Nil{}:
675	      h
676	    case hd <> tl:
677	      internal_or_of_right(Nat.is_eq(hd, x), List.contains(~Nat, ~Nat.is_eq, List.append(&2, Nat, tl, ys), x), internal_mem_append_right(tl, ys, x, h))
678	
679	# The head of a cons is a member of it.
680	law mem_cons_self:
681	  for x: Nat
682	  for -xs: List<&2, Nat>
683	  mem(~Nat, ~Nat.is_eq, x, x <> xs)
684	
685	def mem_cons_self(x, xs):
686	  %Equal.sym(Bool, Nat.is_eq(x, x), True{}, MNat.is_eq_refl(x)) : {Bool.or(_, List.contains(~Nat, ~Nat.is_eq, xs, x)) == True{} : Bool}
687	  {==}
688	
689	# Membership is preserved when a new head is prepended.
690	law mem_cons_of_mem:
691	  for x: Nat
692	  for y: Nat
693	  for -xs: List<&2, Nat>
694	  for h: mem(~Nat, ~Nat.is_eq, x, xs)
695	  mem(~Nat, ~Nat.is_eq, x, y <> xs)
696	
697	def mem_cons_of_mem(x, y, xs, h):
698	  +x = x
699	  internal_or_of_right(Nat.is_eq(y, x), List.contains(~Nat, ~Nat.is_eq, xs, x), h)
700	
701	# Nothing is a member of the empty list.
702	law not_mem_nil:
703	  for -x: Nat
704	  mem(~Nat, ~Nat.is_eq, x, Nil{}) -> Empty
705	
706	def not_mem_nil(x, h):
707	  MNat.internal_false_ne_true(h)
708	
709	# Membership on the left of an append.
710	law mem_append_left:
711	  for xs: List<&2, Nat>
712	  for ys: List<&2, Nat>
713	  for x: Nat
714	  for h: mem(~Nat, ~Nat.is_eq, x, xs)
715	  mem(~Nat, ~Nat.is_eq, x, List.append(&2, Nat, xs, ys))
716	
717	def mem_append_left(xs, ys, x, h):
718	  internal_mem_append_left(xs, ys, x, h)
719	
720	# Membership on the right of an append.
721	law mem_append_right:
722	  for xs: List<&2, Nat>
723	  for ys: List<&2, Nat>
724	  for x: Nat
725	  for h: mem(~Nat, ~Nat.is_eq, x, ys)
726	  mem(~Nat, ~Nat.is_eq, x, List.append(&2, Nat, xs, ys))
727	
728	def mem_append_right(xs, ys, x, h):
729	  internal_mem_append_right(xs, ys, x, h)
730	
731	# The empty list is sorted by any comparator.
732	law sorted_nil:
733	  sorted_by(~Nat, ~Nat.is_le, Nil{})
734	
735	def sorted_nil():
736	  {==}
737	
738	# A singleton list is sorted by any comparator.
739	law sorted_single:
740	  for -x: Nat
741	  sorted_by(~Nat, ~Nat.is_le, [x])
742	
743	def sorted_single(x):
744	  {==}
745	
746	# A sorted tail with an in-order head is sorted.
747	law sorted_cons_cons_intro:
748	  for -x: Nat
749	  for -y: Nat
750	  for -t: List<&2, Nat>
751	  for hxy: MNat.le(x, y)
752	  for hyt: sorted_by(~Nat, ~Nat.is_le, y <> t)
753	  sorted_by(~Nat, ~Nat.is_le, x <> y <> t)
754	
755	def sorted_cons_cons_intro(x, y, t, hxy, hyt):
756	  %Equal.sym(Bool, Nat.is_le(x, y), True{}, hxy) : {Bool.and(_, List.all(~&1, ~(Nat & Nat), ~(p => Nat.is_le(Pair.fst(Nat, Nat, p), Pair.snd(Nat, Nat, p))), List.zip(&2, Nat, &2, Nat, y <> t, t))) == True{} : Bool}
757	  hyt
758	
759	# The head pair of a sorted cons-cons list is in order.
760	law sorted_cons_cons_elim_le:
761	  for x: Nat
762	  for y: Nat
763	  for -t: List<&2, Nat>
764	  for h: sorted_by(~Nat, ~Nat.is_le, x <> y <> t)
765	  MNat.le(x, y)
766	
767	def sorted_cons_cons_elim_le(x, y, t, h):
768	  internal_and_left(Nat.is_le(x, y), List.all(~&1, ~(Nat & Nat), ~(p => Nat.is_le(Pair.fst(Nat, Nat, p), Pair.snd(Nat, Nat, p))), List.zip(&2, Nat, &2, Nat, y <> t, t)), h)
769	
770	# The tail of a sorted cons-cons list is sorted.
771	law sorted_cons_cons_elim_tail:
772	  for x: Nat
773	  for y: Nat
774	  for -t: List<&2, Nat>
775	  for h: sorted_by(~Nat, ~Nat.is_le, x <> y <> t)
776	  sorted_by(~Nat, ~Nat.is_le, y <> t)
777	
778	def sorted_cons_cons_elim_tail(x, y, t, h):
779	  internal_and_right(Nat.is_le(x, y), List.all(~&1, ~(Nat & Nat), ~(p => Nat.is_le(Pair.fst(Nat, Nat, p), Pair.snd(Nat, Nat, p))), List.zip(&2, Nat, &2, Nat, y <> t, t)), h)
780	
781	# A sorted list has a sorted tail.
782	law sorted_tail:
783	  for x: Nat
784	  for xs: List<&2, Nat>
785	  for h: sorted_by(~Nat, ~Nat.is_le, x <> xs)
786	  sorted_by(~Nat, ~Nat.is_le, xs)
787	
788	def sorted_tail(x, xs, h):
789	  match xs:
790	    case Nil{}:
791	      {==}
792	    case y <> t:
793	      internal_and_right(Nat.is_le(x, y), List.all(~&1, ~(Nat & Nat), ~(p => Nat.is_le(Pair.fst(Nat, Nat, p), Pair.snd(Nat, Nat, p))), List.zip(&2, Nat, &2, Nat, y <> t, t)), h)
794	
795	# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
796	
797	# The empty list is a right identity for append: xs ++ [] = xs, reversed to rewrite toward the simple side.
798	law append_nil_sym:
799	  for -a: Quant
800	  for -A: Kind(a)
801	  for xs: List<a, A>
802	  {xs == List.append(a, A, xs, Nil{}) : List<a, A>}
803	
804	def append_nil_sym(a, A, xs):
805	  Equal.sym(List<a, A>, List.append(a, A, xs, Nil{}), xs, append_nil(a, A, xs))
806	
807	# The empty list is a left identity for append: [] ++ xs = xs, reversed to rewrite toward the simple side.
808	law nil_append_sym:
809	  for -a: Quant
810	  for -A: Kind(a)
811	  for -xs: List<a, A>
812	  {xs == List.append(a, A, Nil{}, xs) : List<a, A>}
813	
814	def nil_append_sym(a, A, xs):
815	  Equal.sym(List<a, A>, List.append(a, A, Nil{}, xs), xs, nil_append(a, A, xs))
816	
817	# Append is associative: (xs ++ ys) ++ zs = xs ++ (ys ++ zs), reversed to rewrite toward the simple side.
818	law append_assoc_sym:
819	  for -a: Quant
820	  for -A: Kind(a)
821	  for xs: List<a, A>
822	  for -ys: List<a, A>
823	  for -zs: List<a, A>
824	  {List.append(a, A, xs, List.append(a, A, ys, zs)) == List.append(a, A, List.append(a, A, xs, ys), zs) : List<a, A>}
825	
826	def append_assoc_sym(a, A, xs, ys, zs):
827	  Equal.sym(List<a, A>, List.append(a, A, List.append(a, A, xs, ys), zs), List.append(a, A, xs, List.append(a, A, ys, zs)), append_assoc(a, A, xs, ys, zs))
828	
829	# The length of an append is the sum of the lengths, reversed to rewrite toward the simple side.
830	law length_append_sym:
831	  for -a: Quant
832	  for -A: Kind(a)
833	  for xs: List<a, A>
834	  for -ys: List<a, A>
835	  {Nat.add(List.length(a, A, xs), List.length(a, A, ys)) == List.length(a, A, List.append(a, A, xs, ys)) : Nat}
836	
837	def length_append_sym(a, A, xs, ys):
838	  Equal.sym(Nat, List.length(a, A, List.append(a, A, xs, ys)), Nat.add(List.length(a, A, xs), List.length(a, A, ys)), length_append(a, A, xs, ys))
839	
840	# The reverse accumulator loop appends the reversed list to the accumulator, reversed to rewrite toward the simple side.
841	law reverse_go_spec_sym:
842	  for -a: Quant
843	  for -A: Kind(a)
844	  for xs: List<a, A>
845	  for -acc: List<a, A>
846	  {List.append(a, A, List.reverse(a, A, xs), acc) == List.reverse.go(a, A, xs, acc) : List<a, A>}
847	
848	def reverse_go_spec_sym(a, A, xs, acc):
849	  Equal.sym(List<a, A>, List.reverse.go(a, A, xs, acc), List.append(a, A, List.reverse(a, A, xs), acc), reverse_go_spec(a, A, xs, acc))
850	
851	# Reversing an append reverses and swaps the parts: reverse (xs ++ ys) = reverse ys ++ reverse xs, reversed to rewrite toward the simple side.
852	law reverse_append_sym:
853	  for -a: Quant
854	  for -A: Kind(a)
855	  for xs: List<a, A>
856	  for ys: List<a, A>
857	  {List.append(a, A, List.reverse(a, A, ys), List.reverse(a, A, xs)) == List.reverse(a, A, List.append(a, A, xs, ys)) : List<a, A>}
858	
859	def reverse_append_sym(a, A, xs, ys):
860	  Equal.sym(List<a, A>, List.reverse(a, A, List.append(a, A, xs, ys)), List.append(a, A, List.reverse(a, A, ys), List.reverse(a, A, xs)), reverse_append(a, A, xs, ys))
861	
862	# Reversing twice gives the list back, reversed to rewrite toward the simple side.
863	law reverse_reverse_sym:
864	  for -a: Quant
865	  for -A: Kind(a)
866	  for xs: List<a, A>
867	  {xs == List.reverse(a, A, List.reverse(a, A, xs)) : List<a, A>}
868	
869	def reverse_reverse_sym(a, A, xs):
870	  Equal.sym(List<a, A>, List.reverse(a, A, List.reverse(a, A, xs)), xs, reverse_reverse(a, A, xs))
871	
872	# Reversing preserves the length, reversed to rewrite toward the simple side.
873	law length_reverse_sym:
874	  for -a: Quant
875	  for -A: Kind(a)
876	  for xs: List<a, A>
877	  {List.length(a, A, xs) == List.length(a, A, List.reverse(a, A, xs)) : Nat}
878	
879	def length_reverse_sym(a, A, xs):
880	  Equal.sym(Nat, List.length(a, A, List.reverse(a, A, xs)), List.length(a, A, xs), length_reverse(a, A, xs))
881	
882	# A right fold over an append folds the first part onto the fold of the second, reversed to rewrite toward the simple side.
883	law foldr_append_sym:
884	  for ~a: Quant
885	  for ~A: Kind(a)
886	  for ~B: Type
887	  for ~f: A -> B -> B
888	  for xs: List<a, A>
889	  for -ys: List<a, A>
890	  for -z: B
891	  {List.foldr(~a, ~A, ~B, ~f, xs, List.foldr(~a, ~A, ~B, ~f, ys, z)) == List.foldr(~a, ~A, ~B, ~f, List.append(a, A, xs, ys), z) : B}
892	
893	def foldr_append_sym(a, A, B, f, xs, ys, z):
894	  Equal.sym(B, List.foldr(~a, ~A, ~B, ~f, List.append(a, A, xs, ys), z), List.foldr(~a, ~A, ~B, ~f, xs, List.foldr(~a, ~A, ~B, ~f, ys, z)), foldr_append(~a, ~A, ~B, ~f, xs, ys, z))
895	
896	# Taking n elements and appending the rest after dropping n gives the list back, reversed to rewrite toward the simple side.
897	law take_append_drop_sym:
898	  for -a: Quant
899	  for -A: Kind(a)
900	  for xs: List<a, A>
901	  for n: Nat
902	  {xs == List.append(a, A, List.take(a, A, xs, n), List.drop(a, A, xs, n)) : List<a, A>}
903	
904	def take_append_drop_sym(a, A, xs, n):
905	  Equal.sym(List<a, A>, List.append(a, A, List.take(a, A, xs, n), List.drop(a, A, xs, n)), xs, take_append_drop(a, A, xs, n))
906	
907	# Mapping preserves the length, reversed to rewrite toward the simple side.
908	law length_map_sym:
909	  for ~A: Type
910	  for ~B: Type
911	  for ~f: A -> B
912	  for xs: List<A>
913	  {List.length(&1, A, xs) == List.length(&1, B, List.map(~A, ~B, ~f, xs)) : Nat}
914	
915	def length_map_sym(A, B, f, xs):
916	  Equal.sym(Nat, List.length(&1, B, List.map(~A, ~B, ~f, xs)), List.length(&1, A, xs), length_map(~A, ~B, ~f, xs))
917	
918	# Mapping over an append maps each part: map f (xs ++ ys) = map f xs ++ map f ys, reversed to rewrite toward the simple side.
919	law map_append_sym:
920	  for ~A: Type
921	  for ~B: Type
922	  for ~f: A -> B
923	  for xs: List<A>
924	  for -ys: List<A>
925	  {List.append(&1, B, List.map(~A, ~B, ~f, xs), List.map(~A, ~B, ~f, ys)) == List.map(~A, ~B, ~f, List.append(&1, A, xs, ys)) : List<B>}
926	
927	def map_append_sym(A, B, f, xs, ys):
928	  Equal.sym(List<B>, List.map(~A, ~B, ~f, List.append(&1, A, xs, ys)), List.append(&1, B, List.map(~A, ~B, ~f, xs), List.map(~A, ~B, ~f, ys)), map_append(~A, ~B, ~f, xs, ys))
929	
930	# Mapping twice is mapping the composition: map g (map f xs) = map (g . f) xs, reversed to rewrite toward the simple side.
931	law map_map_sym:
932	  for ~A: Type
933	  for ~B: Type
934	  for ~C: Type
935	  for ~f: A -> B
936	  for ~g: B -> C
937	  for xs: List<A>
938	  {List.map(~A, ~C, ~(x => g(f(x))), xs) == List.map(~B, ~C, ~g, List.map(~A, ~B, ~f, xs)) : List<C>}
939	
940	def map_map_sym(A, B, C, f, g, xs):
941	  Equal.sym(List<C>, List.map(~B, ~C, ~g, List.map(~A, ~B, ~f, xs)), List.map(~A, ~C, ~(x => g(f(x))), xs), map_map(~A, ~B, ~C, ~f, ~g, xs))
942	
943	# Taking zero elements gives the empty list, reversed to rewrite toward the simple side.
944	law take_zero_sym:
945	  for -a: Quant
946	  for -A: Kind(a)
947	  for xs: List<a, A>
948	  {Nil{} == List.take(a, A, xs, 0n) : List<a, A>}
949	
950	def take_zero_sym(a, A, xs):
951	  Equal.sym(List<a, A>, List.take(a, A, xs, 0n), Nil{}, take_zero(a, A, xs))
952	
953	# Dropping zero elements gives the list back, reversed to rewrite toward the simple side.
954	law drop_zero_sym:
955	  for -a: Quant
956	  for -A: Kind(a)
957	  for xs: List<a, A>
958	  {xs == List.drop(a, A, xs, 0n) : List<a, A>}
959	
960	def drop_zero_sym(a, A, xs):
961	  Equal.sym(List<a, A>, List.drop(a, A, xs, 0n), xs, drop_zero(a, A, xs))
962	
963	# Taking from the empty list gives the empty list, reversed to rewrite toward the simple side.
964	law take_nil_sym:
965	  for -a: Quant
966	  for -A: Kind(a)
967	  for -n: Nat
968	  {Nil{} == List.take(a, A, Nil{}, n) : List<a, A>}
969	
970	def take_nil_sym(a, A, n):
971	  Equal.sym(List<a, A>, List.take(a, A, Nil{}, n), Nil{}, take_nil(a, A, n))
972	
973	# Dropping from the empty list gives the empty list, reversed to rewrite toward the simple side.
974	law drop_nil_sym:
975	  for -a: Quant
976	  for -A: Kind(a)
977	  for -n: Nat
978	  {Nil{} == List.drop(a, A, Nil{}, n) : List<a, A>}
979	
980	def drop_nil_sym(a, A, n):
981	  Equal.sym(List<a, A>, List.drop(a, A, Nil{}, n), Nil{}, drop_nil(a, A, n))
982	
983	# Taking n elements leaves min(n, length) of them, reversed to rewrite toward the simple side.
984	law length_take_sym:
985	  for -a: Quant
986	  for -A: Kind(a)
987	  for xs: List<a, A>
988	  for n: Nat
989	  {Nat.min(n, List.length(a, A, xs)) == List.length(a, A, List.take(a, A, xs, n)) : Nat}
990	
991	def length_take_sym(a, A, xs, n):
992	  Equal.sym(Nat, List.length(a, A, List.take(a, A, xs, n)), Nat.min(n, List.length(a, A, xs)), length_take(a, A, xs, n))
993	
994	# Dropping n elements leaves length - n of them, reversed to rewrite toward the simple side.
995	law length_drop_sym:
996	  for -a: Quant
997	  for -A: Kind(a)
998	  for xs: List<a, A>
999	  for n: Nat
1000	  {Nat.sub(List.length(a, A, xs), n) == List.length(a, A, List.drop(a, A, xs, n)) : Nat}
1001	
1002	def length_drop_sym(a, A, xs, n):
1003	  Equal.sym(Nat, List.length(a, A, List.drop(a, A, xs, n)), Nat.sub(List.length(a, A, xs), n), length_drop(a, A, xs, n))
1004	
1005	# Taking as many elements as the list has gives the list back, reversed to rewrite toward the simple side.
1006	law take_length_sym:
1007	  for -A: Data
1008	  for +xs: List<&2, A>
1009	  {xs == List.take(&2, A, xs, List.length(&2, A, xs)) : List<&2, A>}
1010	
1011	def take_length_sym(A, xs):
1012	  Equal.sym(List<&2, A>, List.take(&2, A, xs, List.length(&2, A, xs)), xs, take_length(A, xs))
1013	
1014	# Dropping as many elements as the list has gives the empty list, reversed to rewrite toward the simple side.
1015	law drop_length_sym:
1016	  for -A: Data
1017	  for +xs: List<&2, A>
1018	  {Nil{} == List.drop(&2, A, xs, List.length(&2, A, xs)) : List<&2, A>}
1019	
1020	def drop_length_sym(A, xs):
1021	  Equal.sym(List<&2, A>, List.drop(&2, A, xs, List.length(&2, A, xs)), Nil{}, drop_length(A, xs))
1022	
1023	# Taking m from the first n is taking min(n, m), reversed to rewrite toward the simple side.
1024	law take_take_sym:
1025	  for -a: Quant
1026	  for -A: Kind(a)
1027	  for xs: List<a, A>
1028	  for n: Nat
1029	  for m: Nat
1030	  {List.take(a, A, xs, Nat.min(n, m)) == List.take(a, A, List.take(a, A, xs, n), m) : List<a, A>}
1031	
1032	def take_take_sym(a, A, xs, n, m):
1033	  Equal.sym(List<a, A>, List.take(a, A, List.take(a, A, xs, n), m), List.take(a, A, xs, Nat.min(n, m)), take_take(a, A, xs, n, m))
1034	
1035	# Dropping m after dropping n is dropping n + m, reversed to rewrite toward the simple side.
1036	law drop_drop_sym:
1037	  for -a: Quant
1038	  for -A: Kind(a)
1039	  for xs: List<a, A>
1040	  for n: Nat
1041	  for -m: Nat
1042	  {List.drop(a, A, xs, Nat.add(n, m)) == List.drop(a, A, List.drop(a, A, xs, n), m) : List<a, A>}
1043	
1044	def drop_drop_sym(a, A, xs, n, m):
1045	  Equal.sym(List<a, A>, List.drop(a, A, List.drop(a, A, xs, n), m), List.drop(a, A, xs, Nat.add(n, m)), drop_drop(a, A, xs, n, m))
1046	
1047	# Reversing the empty list gives the empty list, reversed to rewrite toward the simple side.
1048	law reverse_nil_sym:
1049	  for -a: Quant
1050	  for -A: Kind(a)
1051	  {Nil{} == List.reverse(a, A, Nil{}) : List<a, A>}
1052	
1053	def reverse_nil_sym(a, A):
1054	  Equal.sym(List<a, A>, List.reverse(a, A, Nil{}), Nil{}, reverse_nil(a, A))
1055	
1056	# Reversing a one-element list gives it back, reversed to rewrite toward the simple side.
1057	law reverse_singleton_sym:
1058	  for -a: Quant
1059	  for -A: Kind(a)
1060	  for -x: A
1061	  {[x] == List.reverse(a, A, [x]) : List<a, A>}
1062	
1063	def reverse_singleton_sym(a, A, x):
1064	  Equal.sym(List<a, A>, List.reverse(a, A, [x]), [x], reverse_singleton(a, A, x))
1065	
1066	# Replicating x n times gives a list of length n, reversed to rewrite toward the simple side.
1067	law length_replicate_sym:
1068	  for -A: Data
1069	  for n: Nat
1070	  for -x: A
1071	  {n == List.length(&2, A, List.replicate(A, n, x)) : Nat}
1072	
1073	def length_replicate_sym(A, n, x):
1074	  Equal.sym(Nat, List.length(&2, A, List.replicate(A, n, x)), n, length_replicate(A, n, x))
1075	
1076	# Range(n) has length n, reversed to rewrite toward the simple side.
1077	law length_range_sym:
1078	  for n: Nat
1079	  {n == List.length(&2, Nat, List.range(n)) : Nat}
1080	
1081	def length_range_sym(n):
1082	  Equal.sym(Nat, List.length(&2, Nat, List.range(n)), n, length_range(n))
1083	
1084	# Zipping two lists gives the length of the shorter one, reversed to rewrite toward the simple side.
1085	law length_zip_sym:
1086	  for -a: Quant
1087	  for -A: Kind(a)
1088	  for xs: List<a, A>
1089	  for ys: List<a, A>
1090	  {Nat.min(List.length(a, A, xs), List.length(a, A, ys)) == List.length(&1, A & A, List.zip(a, A, a, A, xs, ys)) : Nat}
1091	
1092	def length_zip_sym(a, A, xs, ys):
1093	  Equal.sym(Nat, List.length(&1, A & A, List.zip(a, A, a, A, xs, ys)), Nat.min(List.length(a, A, xs), List.length(a, A, ys)), length_zip(a, A, xs, ys))
1094	
1095	# Appending after a cons: (x :: xs) ++ ys = x :: (xs ++ ys), reversed to rewrite toward the simple side.
1096	law append_cons_sym:
1097	  for -a: Quant
1098	  for -A: Kind(a)
1099	  for -x: A
1100	  for -xs: List<a, A>
1101	  for -ys: List<a, A>
1102	  {x <> List.append(a, A, xs, ys) == List.append(a, A, x <> xs, ys) : List<a, A>}
1103	
1104	def append_cons_sym(a, A, x, xs, ys):
1105	  Equal.sym(List<a, A>, List.append(a, A, x <> xs, ys), x <> List.append(a, A, xs, ys), append_cons(a, A, x, xs, ys))
1106	
1107	# The empty list has length zero, reversed to rewrite toward the simple side.
1108	law length_nil_sym:
1109	  for -a: Quant
1110	  for -A: Kind(a)
1111	  {0n == List.length(a, A, Nil{}) : Nat}
1112	
1113	def length_nil_sym(a, A):
1114	  Equal.sym(Nat, List.length(a, A, Nil{}), 0n, length_nil(a, A))
1115	
1116	# A cons is one longer than its tail, reversed to rewrite toward the simple side.
1117	law length_cons_sym:
1118	  for -a: Quant
1119	  for -A: Kind(a)
1120	  for -x: A
1121	  for -xs: List<a, A>
1122	  {1n+List.length(a, A, xs) == List.length(a, A, x <> xs) : Nat}
1123	
1124	def length_cons_sym(a, A, x, xs):
1125	  Equal.sym(Nat, List.length(a, A, x <> xs), 1n+List.length(a, A, xs), length_cons(a, A, x, xs))
1126	
1127	# Concatenating an append concatenates each part: concat (xss ++ yss) = concat xss ++ concat yss, reversed to rewrite toward the simple side.
1128	law concat_append_sym:
1129	  for -a: Quant
1130	  for -A: Kind(a)
1131	  for xss: List<a, List<a, A>>
1132	  for -yss: List<a, List<a, A>>
1133	  {List.append(a, A, List.concat(a, A, xss), List.concat(a, A, yss)) == List.concat(a, A, List.append(a, List<a, A>, xss, yss)) : List<a, A>}
1134	
1135	def concat_append_sym(a, A, xss, yss):
1136	  Equal.sym(List<a, A>, List.concat(a, A, List.append(a, List<a, A>, xss, yss)), List.append(a, A, List.concat(a, A, xss), List.concat(a, A, yss)), concat_append(a, A, xss, yss))
1137	
1138	# A left fold over an append folds the second part from the fold of the first, reversed to rewrite toward the simple side.
1139	law foldl_append_sym:
1140	  for ~a: Quant
1141	  for ~A: Kind(a)
1142	  for ~B: Type
1143	  for ~f: B -> A -> B
1144	  for xs: List<a, A>
1145	  for -ys: List<a, A>
1146	  for -z: B
1147	  {List.foldl(~a, ~A, ~B, ~f, ys, List.foldl(~a, ~A, ~B, ~f, xs, z)) == List.foldl(~a, ~A, ~B, ~f, List.append(a, A, xs, ys), z) : B}
1148	
1149	def foldl_append_sym(a, A, B, f, xs, ys, z):
1150	  Equal.sym(B, List.foldl(~a, ~A, ~B, ~f, List.append(a, A, xs, ys), z), List.foldl(~a, ~A, ~B, ~f, ys, List.foldl(~a, ~A, ~B, ~f, xs, z)), foldl_append(~a, ~A, ~B, ~f, xs, ys, z))
1151	
1152	# Mapping commutes with reversing: map f (reverse xs) = reverse (map f xs), reversed to rewrite toward the simple side.
1153	law map_reverse_sym:
1154	  for ~A: Type
1155	  for ~B: Type
1156	  for ~f: A -> B
1157	  for xs: List<A>
1158	  {List.reverse(&1, B, List.map(~A, ~B, ~f, xs)) == List.map(~A, ~B, ~f, List.reverse(&1, A, xs)) : List<B>}
1159	
1160	def map_reverse_sym(A, B, f, xs):
1161	  Equal.sym(List<B>, List.map(~A, ~B, ~f, List.reverse(&1, A, xs)), List.reverse(&1, B, List.map(~A, ~B, ~f, xs)), map_reverse(~A, ~B, ~f, xs))
1162	
1163	# All over an append is all over each part, joined by and, reversed to rewrite toward the simple side.
1164	law all_append_sym:
1165	  for ~a: Quant
1166	  for ~A: Kind(a)
1167	  for ~f: A -> Bool
1168	  for xs: List<a, A>
1169	  for -ys: List<a, A>
1170	  {Bool.and(List.all(~a, ~A, ~f, xs), List.all(~a, ~A, ~f, ys)) == List.all(~a, ~A, ~f, List.append(a, A, xs, ys)) : Bool}
1171	
1172	def all_append_sym(a, A, f, xs, ys):
1173	  Equal.sym(Bool, List.all(~a, ~A, ~f, List.append(a, A, xs, ys)), Bool.and(List.all(~a, ~A, ~f, xs), List.all(~a, ~A, ~f, ys)), all_append(~a, ~A, ~f, xs, ys))
1174	
1175	# Any over an append is any over each part, joined by or, reversed to rewrite toward the simple side.
1176	law any_append_sym:
1177	  for ~a: Quant
1178	  for ~A: Kind(a)
1179	  for ~f: A -> Bool
1180	  for xs: List<a, A>
1181	  for -ys: List<a, A>
1182	  {Bool.or(List.any(~a, ~A, ~f, xs), List.any(~a, ~A, ~f, ys)) == List.any(~a, ~A, ~f, List.append(a, A, xs, ys)) : Bool}
1183	
1184	def any_append_sym(a, A, f, xs, ys):
1185	  Equal.sym(Bool, List.any(~a, ~A, ~f, List.append(a, A, xs, ys)), Bool.or(List.any(~a, ~A, ~f, xs), List.any(~a, ~A, ~f, ys)), any_append(~a, ~A, ~f, xs, ys))
1186	
1187	# Filtering an append filters each part, reversed to rewrite toward the simple side.
1188	law filter_append_sym:
1189	  for ~A: Data
1190	  for ~f: A -> Bool
1191	  for xs: List<&2, A>
1192	  for ys: List<&2, A>
1193	  {List.append(&2, A, List.filter(~A, ~f, xs), List.filter(~A, ~f, ys)) == List.filter(~A, ~f, List.append(&2, A, xs, ys)) : List<&2, A>}
1194	
1195	def filter_append_sym(A, f, xs, ys):
1196	  Equal.sym(List<&2, A>, List.filter(~A, ~f, List.append(&2, A, xs, ys)), List.append(&2, A, List.filter(~A, ~f, xs), List.filter(~A, ~f, ys)), filter_append(~A, ~f, xs, ys))
1197	
1198	# An append contains x iff either part does, reversed to rewrite toward the simple side.
1199	law contains_append_sym:
1200	  for ~A: Data
1201	  for ~eq: A -> A -> Bool
1202	  for xs: List<&2, A>
1203	  for -ys: List<&2, A>
1204	  for +x: A
1205	  {Bool.or(List.contains(~A, ~eq, xs, x), List.contains(~A, ~eq, ys, x)) == List.contains(~A, ~eq, List.append(&2, A, xs, ys), x) : Bool}
1206	
1207	def contains_append_sym(A, eq, xs, ys, x):
1208	  Equal.sym(Bool, List.contains(~A, ~eq, List.append(&2, A, xs, ys), x), Bool.or(List.contains(~A, ~eq, xs, x), List.contains(~A, ~eq, ys, x)), contains_append(~A, ~eq, xs, ys, x))
1209	
1210	# Filtering never makes a list longer, reversed to rewrite toward the simple side.
1211	law length_filter_le_sym:
1212	  for ~A: Data
1213	  for ~f: A -> Bool
1214	  for xs: List<&2, A>
1215	  {True{} == Nat.is_le(List.length(&2, A, List.filter(~A, ~f, xs)), List.length(&2, A, xs)) : Bool}
1216	
1217	def length_filter_le_sym(A, f, xs):
1218	  Equal.sym(Bool, Nat.is_le(List.length(&2, A, List.filter(~A, ~f, xs)), List.length(&2, A, xs)), True{}, length_filter_le(~A, ~f, xs))