1	import Base
2	
3	def append_nil(-A: Data, +xs: List<&2, A>) -> {List.append(&2, A, xs, Nil{}) == xs : List<&2, A>}:
4	    match xs:
5	        case Nil{}: {==}
6	        case h <> t:
7	            Equal.cong(List<&2, A>, List<&2, A>, ys => h <> ys, List.append(&2, A, t, Nil{}), t, append_nil(A, t))
8	
9	def append_assoc(-A: Data,
10	                 +xs: List<&2, A>,
11	                 +ys: List<&2, A>,
12	                 +zs: List<&2, A>) -> {List.append(&2, A, List.append(&2, A, xs, ys), zs) == List.append(&2, A, xs, List.append(&2, A, ys, zs)) : List<&2, A>}:
13	    match xs:
14	        case Nil{}: {==}
15	        case h <> t:
16	            Equal.cong(List<&2, A>, List<&2, A>, q => h <> q,
17	                List.append(&2, A, List.append(&2, A, t, ys), zs), List.append(&2, A, t, List.append(&2, A, ys, zs)), append_assoc(A, t, ys, zs))
18	
19	def reverse_shift(-A: Data,
20	                  +xs: List<&2, A>,
21	                  +acc: List<&2, A>,
22	                  +tail: List<&2, A>) -> {List.reverse.go(&2, A, List.reverse.go(&2, A, xs, acc), tail) == List.reverse.go(&2, A, acc, List.append(&2, A, xs, tail)) : List<&2, A>}:
23	    match xs:
24	        case Nil{}: {==}
25	        case h <> t: reverse_shift(A, t, h <> acc, tail)
26	
27	def reverse_go_append(-A: Data,
28	                      +xs: List<&2, A>,
29	                      +acc: List<&2, A>,
30	                      +tail: List<&2, A>) -> {List.reverse.go(&2, A, xs, List.append(&2, A, acc, tail)) == List.append(&2, A, List.reverse.go(&2, A, xs, acc), tail) : List<&2, A>}:
31	    match xs:
32	        case Nil{}: {==}
33	        case h <> t:
34	            reverse_go_append(A, t, h <> acc, tail)
35	
36	def reverse_cons(-A: Data,
37	                 +head: A,
38	                 +tail: List<&2, A>) -> {List.reverse(&2, A, head <> tail) == List.append(&2, A, List.reverse(&2, A, tail), head <> Nil{}) : List<&2, A>}:
39	    reverse_go_append(A, tail, Nil{}, head <> Nil{})
40	
41	def reverse_append(-A: Data,
42	                   +xs: List<&2, A>,
43	                   +ys: List<&2, A>) -> {List.reverse(&2, A, List.append(&2, A, xs, ys)) == List.append(&2, A, List.reverse(&2, A, ys), List.reverse(&2, A, xs)) : List<&2, A>}:
44	    match xs:
45	        case Nil{}:
46	            Equal.sym(List<&2, A>, List.append(&2, A, List.reverse(&2, A, ys), Nil{}),
47	                List.reverse(&2, A, ys),
48	                append_nil(A, List.reverse(&2, A, ys)))
49	        case h <> t:
50	            Equal.trans(List<&2, A>,
51	                List.reverse(&2, A, List.append(&2, A, h <> t, ys)),
52	                List.append(&2, A, List.reverse(&2, A, List.append(&2, A, t, ys)), h <> Nil{}),
53	                List.append(&2, A, List.reverse(&2, A, ys), List.reverse(&2, A, h <> t)),
54	                reverse_go_append(A, List.append(&2, A, t, ys), Nil{}, h <> Nil{}),
55	                Equal.trans(List<&2, A>,
56	                    List.append(&2, A, List.reverse(&2, A, List.append(&2, A, t, ys)), h <> Nil{}),
57	                    List.append(&2, A, List.append(&2, A, List.reverse(&2, A, ys), List.reverse(&2, A, t)), h <> Nil{}),
58	                    List.append(&2, A, List.reverse(&2, A, ys), List.reverse(&2, A, h <> t)),
59	                    Equal.cong(List<&2, A>, List<&2, A>, xs => List.append(&2, A, xs, h <> Nil{}),
60	                        List.reverse(&2, A, List.append(&2, A, t, ys)),
61	                        List.append(&2, A, List.reverse(&2, A, ys), List.reverse(&2, A, t)),
62	                        reverse_append(A, t, ys)),
63	                    Equal.trans(List<&2, A>,
64	                        List.append(&2, A, List.append(&2, A, List.reverse(&2, A, ys), List.reverse(&2, A, t)), h <> Nil{}),
65	                        List.append(&2, A, List.reverse(&2, A, ys), List.append(&2, A, List.reverse(&2, A, t), h <> Nil{})),
66	                        List.append(&2, A, List.reverse(&2, A, ys), List.reverse(&2, A, h <> t)),
67	                        append_assoc(A, List.reverse(&2, A, ys), List.reverse(&2, A, t), h <> Nil{}),
68	                        Equal.cong(List<&2, A>, List<&2, A>, xs => List.append(&2, A, List.reverse(&2, A, ys), xs),
69	                            List.append(&2, A, List.reverse(&2, A, t), h <> Nil{}),
70	                            List.reverse(&2, A, h <> t),
71	                            Equal.sym(List<&2, A>,
72	                                List.reverse(&2, A, h <> t),
73	                                List.append(&2, A, List.reverse(&2, A, t), h <> Nil{}),
74	                                reverse_go_append(A, t, Nil{}, h <> Nil{}))))))
75	
76	def reverse_twice(-A: Data,
77	                  +xs: List<&2, A>) -> {List.reverse(&2, A, List.reverse(&2, A, xs)) == xs : List<&2, A>}:
78	    Equal.trans(List<&2, A>, List.reverse(&2, A, List.reverse(&2, A, xs)), List.append(&2, A, xs, Nil{}), xs,
79	        reverse_shift(A, xs, Nil{}, Nil{}), append_nil(A, xs))