1	# Proofs of LAWS.bend. Internal lemmas are prefixed AP.
2	#
3	# The method: an array is reflected, once, into a Data tree (AP.Tree) with an
4	# equation between the tree's array and the array, so that the lemmas can
5	# mention it as often as they need. On the tree, AP.size, AP.swap_t,
6	# AP.swap_v and AP.get_v mirror Base's Array.size, Array.swap.go and
7	# Array.get.go with the same index arithmetic, so Base's code on a built tree
8	# is the mirror by plain induction. For the list model, the index arithmetic
9	# is tied to the indices' values: U32's order is its value's order, Word.sub
10	# subtracts, halving 2^(d+1) gives 2^d, and 2^d - 1 masks the low d bits.
11	import Base
12	import ./array.bend as A
13	import ./LAWS.bend as Laws
14	
15	def AP.bool_t(b: Bool) -> Type:
16	  match b:
17	    case True{}:
18	      Unit
19	    case False{}:
20	      Empty
21	
22	def AP.ft(e: {False{} == True{} : Bool}) -> Empty:
23	  %Equal.sym(Bool, False{}, True{}, e) : AP.bool_t(_)
24	  Unit{}
25	
26	def AP.tf(e: {True{} == False{} : Bool}) -> Empty:
27	  %e : AP.bool_t(_)
28	  Unit{}
29	
30	def AP.nat_t(n: Nat) -> Type:
31	  match n:
32	    case 0n:
33	      Unit
34	    case 1n+p:
35	      Empty
36	
37	# 1 + k is never 0
38	def AP.sz(-k: Nat, e: {1n+k == 0n : Nat}) -> Empty:
39	  %Equal.sym(Nat, 1n+k, 0n, e) : AP.nat_t(_)
40	  Unit{}
41	
42	def AP.succ_cong(-a: Nat, -b: Nat, e: {a == b : Nat}) -> {1n+a == 1n+b : Nat}:
43	  %e : {1n+a == 1n+_ : Nat}
44	  {==}
45	
46	def AP.double_cong(-a: Nat, -b: Nat, e: {a == b : Nat}) -> {Nat.double(a) == Nat.double(b) : Nat}:
47	  %e : {Nat.double(a) == Nat.double(_) : Nat}
48	  {==}
49	
50	# Nat arithmetic
51	
52	def AP.add_zero(x: Nat) -> {Nat.add(x, 0n) == x : Nat}:
53	  match x:
54	    case 0n:
55	      {==}
56	    case 1n+p:
57	      AP.succ_cong(Nat.add(p, 0n), p, AP.add_zero(p))
58	
59	def AP.add_succ(x: Nat, -y: Nat) -> {Nat.add(x, 1n+y) == 1n+Nat.add(x, y) : Nat}:
60	  match x:
61	    case 0n:
62	      {==}
63	    case 1n+p:
64	      AP.succ_cong(Nat.add(p, 1n+y), 1n+Nat.add(p, y), AP.add_succ(p, y))
65	
66	def AP.add_comm(x: Nat, +y: Nat) -> {Nat.add(x, y) == Nat.add(y, x) : Nat}:
67	  match x:
68	    case 0n:
69	      Equal.sym(Nat, Nat.add(y, 0n), y, AP.add_zero(y))
70	    case 1n+p:
71	      Equal.trans(Nat, 1n+Nat.add(p, y), 1n+Nat.add(y, p), Nat.add(y, 1n+p), AP.succ_cong(Nat.add(p, y), Nat.add(y, p), AP.add_comm(p, y)), Equal.sym(Nat, Nat.add(y, 1n+p), 1n+Nat.add(y, p), AP.add_succ(y, p)))
72	
73	def AP.double_add(x: Nat, -y: Nat) -> {Nat.double(Nat.add(x, y)) == Nat.add(Nat.double(x), Nat.double(y)) : Nat}:
74	  match x:
75	    case 0n:
76	      {==}
77	    case 1n+p:
78	      AP.succ_cong(1n+Nat.double(Nat.add(p, y)), 1n+Nat.add(Nat.double(p), Nat.double(y)), AP.succ_cong(Nat.double(Nat.add(p, y)), Nat.add(Nat.double(p), Nat.double(y)), AP.double_add(p, y)))
79	
80	def AP.double_self(+x: Nat) -> {Nat.double(x) == Nat.add(x, x) : Nat}:
81	  match x:
82	    case 0n:
83	      {==}
84	    case 1n+p:
85	      %Equal.sym(Nat, Nat.add(p, 1n+p), 1n+Nat.add(p, p), AP.add_succ(p, p)) : {2n+Nat.double(p) == 1n+_ : Nat}
86	      AP.succ_cong(1n+Nat.double(p), 1n+Nat.add(p, p), AP.succ_cong(Nat.double(p), Nat.add(p, p), AP.double_self(p)))
87	
88	def AP.sub_add_l(y: Nat, +r: Nat) -> {Nat.sub(Nat.add(y, r), y) == r : Nat}:
89	  match y:
90	    case 0n:
91	      match r:
92	        case 0n:
93	          {==}
94	        case 1n+q:
95	          {==}
96	    case 1n+q:
97	      AP.sub_add_l(q, r)
98	
99	def AP.sub_add(+r: Nat, +y: Nat) -> {Nat.sub(Nat.add(r, y), y) == r : Nat}:
100	  %AP.add_comm(y, r) : {Nat.sub(_, y) == r : Nat}
101	  AP.sub_add_l(y, r)
102	
103	def AP.lt_cancel(s: Nat, -r: Nat, -u: Nat) -> {Nat.is_lt(Nat.add(s, r), Nat.add(s, u)) == Nat.is_lt(r, u) : Bool}:
104	  match s:
105	    case 0n:
106	      {==}
107	    case 1n+q:
108	      AP.lt_cancel(q, r, u)
109	
110	def AP.le_succ(y: Nat, x: Nat) -> {Nat.is_le(1n+y, x) == Nat.is_lt(y, x) : Bool}:
111	  match y x:
112	    case 0n 0n:
113	      {==}
114	    case 0n 1n+p:
115	      match p:
116	        case 0n:
117	          {==}
118	        case 1n+q:
119	          {==}
120	    case 1n+q 0n:
121	      {==}
122	    case 1n+q 1n+p:
123	      AP.le_succ(q, p)
124	
125	def AP.not_lt_le(x: Nat, y: Nat, e: {Nat.is_lt(x, y) == False{} : Bool}) -> {Nat.is_le(y, x) == True{} : Bool}:
126	  match x y:
127	    case 0n 0n:
128	      {==}
129	    case 0n 1n+q:
130	      Empty.absurd({Nat.is_le(1n+q, 0n) == True{} : Bool}, AP.tf(e))
131	    case 1n+p 0n:
132	      {==}
133	    case 1n+p 1n+q:
134	      AP.not_lt_le(p, q, e)
135	
136	def AP.lt_one(x: Nat, e: {Nat.is_lt(x, 1n) == True{} : Bool}) -> {x == 0n : Nat}:
137	  match x:
138	    case 0n:
139	      {==}
140	    case 1n+p:
141	      match p:
142	        case 0n:
143	          Empty.absurd({1n == 0n : Nat}, AP.ft(e))
144	        case 1n+q:
145	          Empty.absurd({2n+q == 0n : Nat}, AP.ft(e))
146	
147	def AP.double_zero(x: Nat, e: {Nat.double(x) == 0n : Nat}) -> {x == 0n : Nat}:
148	  match x:
149	    case 0n:
150	      {==}
151	    case 1n+p:
152	      Empty.absurd({1n+p == 0n : Nat}, AP.sz(1n+Nat.double(p), e))
153	
154	# the value of a word's lowest bit and the rest: Word.to_nat of WCon{b, t}
155	
156	def AP.bv(b: Bool, x: Nat) -> Nat:
157	  match b:
158	    case False{}:
159	      Nat.double(x)
160	    case True{}:
161	      1n+Nat.double(x)
162	
163	def AP.nc(x: Nat, y: Nat, a: Bool, b: Bool) -> {Nat.cmp(AP.bv(a, x), AP.bv(b, y)) == Word.cmp.fin(a, b, Nat.cmp(x, y)) : Cmp}:
164	  match x y:
165	    case 0n 0n:
166	      match a b:
167	        case False{} False{}:
168	          {==}
169	        case False{} True{}:
170	          {==}
171	        case True{} False{}:
172	          {==}
173	        case True{} True{}:
174	          {==}
175	    case 0n 1n+q:
176	      match a b:
177	        case False{} False{}:
178	          {==}
179	        case False{} True{}:
180	          {==}
181	        case True{} False{}:
182	          {==}
183	        case True{} True{}:
184	          {==}
185	    case 1n+p 0n:
186	      match a b:
187	        case False{} False{}:
188	          {==}
189	        case False{} True{}:
190	          {==}
191	        case True{} False{}:
192	          {==}
193	        case True{} True{}:
194	          {==}
195	    case 1n+p 1n+q:
196	      match a b:
197	        case False{} False{}:
198	          AP.nc(p, q, False{}, False{})
199	        case False{} True{}:
200	          AP.nc(p, q, False{}, True{})
201	        case True{} False{}:
202	          AP.nc(p, q, True{}, False{})
203	        case True{} True{}:
204	          AP.nc(p, q, True{}, True{})
205	
206	def AP.vc(-p: Nat, b: Bool, -t: Word(p)) -> {AP.bv(b, Word.to_nat(p, t)) == Word.to_nat(1n+p, WCon{b, t}) : Nat}:
207	  match b:
208	    case False{}:
209	      {==}
210	    case True{}:
211	      {==}
212	
213	# Word.cmp is the order of the words' values
214	
215	def AP.cmp_nat(n: Nat, a: Word(n), b: Word(n)) -> {Word.cmp(n, a, b) == Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) : Cmp}:
216	  match n:
217	    case 0n:
218	      {==}
219	    case 1n+ +p:
220	      match a b:
221	        case WCon{+x, +at} WCon{+y, +bt}:
222	          +xv = Word.to_nat(p, at)
223	          +yv = Word.to_nat(p, bt)
224	          %Equal.sym(Cmp, Word.cmp(p, at, bt), Nat.cmp(xv, yv), AP.cmp_nat(p, at, bt)) : {Word.cmp.fin(x, y, _) == Nat.cmp(Word.to_nat(1n+p, WCon{x, at}), Word.to_nat(1n+p, WCon{y, bt})) : Cmp}
225	          %AP.vc(p, x, at) : {Word.cmp.fin(x, y, Nat.cmp(xv, yv)) == Nat.cmp(_, Word.to_nat(1n+p, WCon{y, bt})) : Cmp}
226	          %AP.vc(p, y, bt) : {Word.cmp.fin(x, y, Nat.cmp(xv, yv)) == Nat.cmp(AP.bv(x, xv), _) : Cmp}
227	          Equal.sym(Cmp, Nat.cmp(AP.bv(x, xv), AP.bv(y, yv)), Word.cmp.fin(x, y, Nat.cmp(xv, yv)), AP.nc(xv, yv, x, y))
228	
229	# U32's order is its value's order
230	
231	def AP.u32_cmp(a: U32, b: U32) -> {U32.cmp(a, b) == Nat.cmp(U32.to_nat(a), U32.to_nat(b)) : Cmp}:
232	  match a b:
233	    case U32{x} U32{y}:
234	      AP.cmp_nat(32n, x, y)
235	
236	def AP.u32_lt(+a: U32, +b: U32) -> {U32.is_lt(a, b) == Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) : Bool}:
237	  %AP.u32_cmp(a, b) : {Cmp.is_lt(U32.cmp(a, b)) == Cmp.is_lt(_) : Bool}
238	  {==}
239	
240	def AP.u32_eq(+a: U32, +b: U32) -> {U32.is_eq(a, b) == Nat.is_eq(U32.to_nat(a), U32.to_nat(b)) : Bool}:
241	  %AP.u32_cmp(a, b) : {Cmp.is_eq(U32.cmp(a, b)) == Cmp.is_eq(_) : Bool}
242	  {==}
243	
244	# Subtraction: Word.adc with a complemented second operand subtracts
245	
246	def AP.cb(c: Bool) -> Nat:
247	  match c:
248	    case True{}:
249	      0n
250	    case False{}:
251	      1n
252	
253	def AP.fin_le_ff(c: Cmp) -> {Cmp.is_le(Word.cmp.fin(False{}, False{}, c)) == Cmp.is_le(c) : Bool}:
254	  match c:
255	    case LT{}:
256	      {==}
257	    case EQ{}:
258	      {==}
259	    case GT{}:
260	      {==}
261	
262	def AP.fin_le_tf(c: Cmp) -> {Cmp.is_le(Word.cmp.fin(True{}, False{}, c)) == Cmp.is_lt(c) : Bool}:
263	  match c:
264	    case LT{}:
265	      {==}
266	    case EQ{}:
267	      {==}
268	    case GT{}:
269	      {==}
270	
271	def AP.fin_le_ft(c: Cmp) -> {Cmp.is_le(Word.cmp.fin(False{}, True{}, c)) == Cmp.is_le(c) : Bool}:
272	  match c:
273	    case LT{}:
274	      {==}
275	    case EQ{}:
276	      {==}
277	    case GT{}:
278	      {==}
279	
280	def AP.fin_lt_xf(b: Bool, c: Cmp) -> {Cmp.is_lt(Word.cmp.fin(b, False{}, c)) == Cmp.is_lt(c) : Bool}:
281	  match b c:
282	    case False{} LT{}:
283	      {==}
284	    case False{} EQ{}:
285	      {==}
286	    case False{} GT{}:
287	      {==}
288	    case True{} LT{}:
289	      {==}
290	    case True{} EQ{}:
291	      {==}
292	    case True{} GT{}:
293	      {==}
294	
295	def AP.le_bits(+y: Nat, +x: Nat, +a: Bool, +b: Bool, h: {Nat.is_le(AP.bv(a, y), AP.bv(b, x)) == True{} : Bool}) -> {Cmp.is_le(Word.cmp.fin(a, b, Nat.cmp(y, x))) == True{} : Bool}:
296	  %AP.nc(y, x, a, b) : {Cmp.is_le(_) == True{} : Bool}
297	  h
298	
299	def AP.lt_bits(+y: Nat, +x: Nat, +a: Bool, +b: Bool, h: {Nat.is_lt(AP.bv(a, y), AP.bv(b, x)) == True{} : Bool}) -> {Cmp.is_lt(Word.cmp.fin(a, b, Nat.cmp(y, x))) == True{} : Bool}:
300	  %AP.nc(y, x, a, b) : {Cmp.is_lt(_) == True{} : Bool}
301	  h
302	
303	def AP.ha(+y: Nat, +x: Nat, h: {Nat.is_le(AP.bv(False{}, y), AP.bv(False{}, x)) == True{} : Bool}) -> {Nat.is_le(y, x) == True{} : Bool}:
304	  %AP.fin_le_ff(Nat.cmp(y, x)) : {_ == True{} : Bool}
305	  AP.le_bits(y, x, False{}, False{}, h)
306	
307	def AP.hb(+y: Nat, +x: Nat, h: {Nat.is_le(AP.bv(True{}, y), AP.bv(False{}, x)) == True{} : Bool}) -> {Nat.is_le(1n+y, x) == True{} : Bool}:
308	  %Equal.sym(Bool, Nat.is_le(1n+y, x), Nat.is_lt(y, x), AP.le_succ(y, x)) : {_ == True{} : Bool}
309	  %AP.fin_le_tf(Nat.cmp(y, x)) : {_ == True{} : Bool}
310	  AP.le_bits(y, x, True{}, False{}, h)
311	
312	def AP.hc(+y: Nat, +x: Nat, h: {Nat.is_le(AP.bv(False{}, y), AP.bv(True{}, x)) == True{} : Bool}) -> {Nat.is_le(y, x) == True{} : Bool}:
313	  %AP.fin_le_ft(Nat.cmp(y, x)) : {_ == True{} : Bool}
314	  AP.le_bits(y, x, False{}, True{}, h)
315	
316	def AP.alg2(+r: Nat, +y: Nat) -> {Nat.double(Nat.add(r, 1n+y)) == Nat.add(1n+Nat.double(r), 1n+Nat.double(y)) : Nat}:
317	  %Equal.sym(Nat, Nat.add(r, 1n+y), 1n+Nat.add(r, y), AP.add_succ(r, y)) : {Nat.double(_) == Nat.add(1n+Nat.double(r), 1n+Nat.double(y)) : Nat}
318	  %Equal.sym(Nat, Nat.add(Nat.double(r), 1n+Nat.double(y)), 1n+Nat.add(Nat.double(r), Nat.double(y)), AP.add_succ(Nat.double(r), Nat.double(y))) : {Nat.double(1n+Nat.add(r, y)) == 1n+_ : Nat}
319	  AP.succ_cong(1n+Nat.double(Nat.add(r, y)), 1n+Nat.add(Nat.double(r), Nat.double(y)), AP.succ_cong(Nat.double(Nat.add(r, y)), Nat.add(Nat.double(r), Nat.double(y)), AP.double_add(r, y)))
320	
321	def AP.alg4(+r: Nat, +y: Nat) -> {Nat.double(Nat.add(r, 1n+y)) == Nat.add(Nat.double(r), 2n+Nat.double(y)) : Nat}:
322	  %Equal.sym(Nat, Nat.add(r, 1n+y), 1n+Nat.add(r, y), AP.add_succ(r, y)) : {Nat.double(_) == Nat.add(Nat.double(r), 2n+Nat.double(y)) : Nat}
323	  %Equal.sym(Nat, Nat.add(Nat.double(r), 2n+Nat.double(y)), 1n+Nat.add(Nat.double(r), 1n+Nat.double(y)), AP.add_succ(Nat.double(r), 1n+Nat.double(y))) : {Nat.double(1n+Nat.add(r, y)) == _ : Nat}
324	  %Equal.sym(Nat, Nat.add(Nat.double(r), 1n+Nat.double(y)), 1n+Nat.add(Nat.double(r), Nat.double(y)), AP.add_succ(Nat.double(r), Nat.double(y))) : {Nat.double(1n+Nat.add(r, y)) == 1n+_ : Nat}
325	  AP.succ_cong(1n+Nat.double(Nat.add(r, y)), 1n+Nat.add(Nat.double(r), Nat.double(y)), AP.succ_cong(Nat.double(Nat.add(r, y)), Nat.add(Nat.double(r), Nat.double(y)), AP.double_add(r, y)))
326	
327	def AP.alg6(+r: Nat, +y: Nat) -> {1n+Nat.double(Nat.add(r, y)) == Nat.add(Nat.double(r), 1n+Nat.double(y)) : Nat}:
328	  %Equal.sym(Nat, Nat.add(Nat.double(r), 1n+Nat.double(y)), 1n+Nat.add(Nat.double(r), Nat.double(y)), AP.add_succ(Nat.double(r), Nat.double(y))) : {1n+Nat.double(Nat.add(r, y)) == _ : Nat}
329	  AP.succ_cong(Nat.double(Nat.add(r, y)), Nat.add(Nat.double(r), Nat.double(y)), AP.double_add(r, y))
330	
331	# for b <= a (b < a when the carry in c is False):
332	# a = adc(a, b, True, c) + (1 - c) + b
333	def AP.adc(n: Nat, a: Word(n), b: Word(n), c: Bool, h: {Nat.is_le(Nat.add(AP.cb(c), Word.to_nat(n, b)), Word.to_nat(n, a)) == True{} : Bool}) -> {Word.to_nat(n, a) == Nat.add(Word.to_nat(n, Word.adc(n, a, b, True{}, c)), Nat.add(AP.cb(c), Word.to_nat(n, b))) : Nat}:
334	  match n:
335	    case 0n:
336	      match a b c:
337	        case WNil{} WNil{} True{}:
338	          {==}
339	        case WNil{} WNil{} False{}:
340	          Empty.absurd({0n == 1n : Nat}, AP.ft(h))
341	    case 1n+ +p:
342	      match a b c:
343	        case WCon{False{}, +at} WCon{False{}, +bt} True{}:
344	          +xv = Word.to_nat(p, at)
345	          +yv = Word.to_nat(p, bt)
346	          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, True{}))
347	          %Equal.sym(Nat, xv, Nat.add(r, yv), AP.adc(p, at, bt, True{}, AP.ha(yv, xv, h))) : {Nat.double(_) == Nat.add(Nat.double(r), Nat.double(yv)) : Nat}
348	          AP.double_add(r, yv)
349	        case WCon{False{}, +at} WCon{True{}, +bt} True{}:
350	          +xv = Word.to_nat(p, at)
351	          +yv = Word.to_nat(p, bt)
352	          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, False{}))
353	          %Equal.sym(Nat, xv, Nat.add(r, 1n+yv), AP.adc(p, at, bt, False{}, AP.hb(yv, xv, h))) : {Nat.double(_) == Nat.add(1n+Nat.double(r), 1n+Nat.double(yv)) : Nat}
354	          AP.alg2(r, yv)
355	        case WCon{True{}, +at} WCon{False{}, +bt} True{}:
356	          +xv = Word.to_nat(p, at)
357	          +yv = Word.to_nat(p, bt)
358	          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, True{}))
359	          %Equal.sym(Nat, xv, Nat.add(r, yv), AP.adc(p, at, bt, True{}, AP.hc(yv, xv, h))) : {1n+Nat.double(_) == 1n+Nat.add(Nat.double(r), Nat.double(yv)) : Nat}
360	          AP.succ_cong(Nat.double(Nat.add(r, yv)), Nat.add(Nat.double(r), Nat.double(yv)), AP.double_add(r, yv))
361	        case WCon{True{}, +at} WCon{True{}, +bt} True{}:
362	          +xv = Word.to_nat(p, at)
363	          +yv = Word.to_nat(p, bt)
364	          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, True{}))
365	          %Equal.sym(Nat, xv, Nat.add(r, yv), AP.adc(p, at, bt, True{}, AP.ha(yv, xv, h))) : {1n+Nat.double(_) == Nat.add(Nat.double(r), 1n+Nat.double(yv)) : Nat}
366	          AP.alg6(r, yv)
367	        case WCon{False{}, +at} WCon{False{}, +bt} False{}:
368	          +xv = Word.to_nat(p, at)
369	          +yv = Word.to_nat(p, bt)
370	          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, False{}))
371	          %Equal.sym(Nat, xv, Nat.add(r, 1n+yv), AP.adc(p, at, bt, False{}, AP.hb(yv, xv, h))) : {Nat.double(_) == Nat.add(1n+Nat.double(r), 1n+Nat.double(yv)) : Nat}
372	          AP.alg2(r, yv)
373	        case WCon{False{}, +at} WCon{True{}, +bt} False{}:
374	          +xv = Word.to_nat(p, at)
375	          +yv = Word.to_nat(p, bt)
376	          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, False{}))
377	          %Equal.sym(Nat, xv, Nat.add(r, 1n+yv), AP.adc(p, at, bt, False{}, AP.ha(1n+yv, xv, h))) : {Nat.double(_) == Nat.add(Nat.double(r), 2n+Nat.double(yv)) : Nat}
378	          AP.alg4(r, yv)
379	        case WCon{True{}, +at} WCon{False{}, +bt} False{}:
380	          +xv = Word.to_nat(p, at)
381	          +yv = Word.to_nat(p, bt)
382	          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, True{}))
383	          %Equal.sym(Nat, xv, Nat.add(r, yv), AP.adc(p, at, bt, True{}, AP.ha(yv, xv, h))) : {1n+Nat.double(_) == Nat.add(Nat.double(r), 1n+Nat.double(yv)) : Nat}
384	          AP.alg6(r, yv)
385	        case WCon{True{}, +at} WCon{True{}, +bt} False{}:
386	          +xv = Word.to_nat(p, at)
387	          +yv = Word.to_nat(p, bt)
388	          +r = Word.to_nat(p, Word.adc(p, at, bt, True{}, False{}))
389	          %Equal.sym(Nat, xv, Nat.add(r, 1n+yv), AP.adc(p, at, bt, False{}, AP.hb(yv, xv, h))) : {1n+Nat.double(_) == 1n+Nat.add(Nat.double(r), 2n+Nat.double(yv)) : Nat}
390	          AP.succ_cong(Nat.double(Nat.add(r, 1n+yv)), Nat.add(Nat.double(r), 2n+Nat.double(yv)), AP.alg4(r, yv))
391	
392	def AP.u32_sub(a: U32, b: U32, h: {Nat.is_le(U32.to_nat(b), U32.to_nat(a)) == True{} : Bool}) -> {U32.to_nat(U32.sub(a, b)) == Nat.sub(U32.to_nat(a), U32.to_nat(b)) : Nat}:
393	  match a b:
394	    case U32{+x} U32{+y}:
395	      +xv = Word.to_nat(32n, x)
396	      +yv = Word.to_nat(32n, y)
397	      +r = Word.to_nat(32n, Word.adc(32n, x, y, True{}, True{}))
398	      %Equal.sym(Nat, xv, Nat.add(r, yv), AP.adc(32n, x, y, True{}, h)) : {r == Nat.sub(_, yv) : Nat}
399	      Equal.sym(Nat, Nat.sub(Nat.add(r, yv), yv), r, AP.sub_add(r, yv))
400	
401	def AP.wcon_cong(-p: Nat, -b: Bool, -x: Word(p), -y: Word(p), e: {x == y : Word(p)}) -> {WCon{b, x} == WCon{b, y} : Word(1n+p)}:
402	  %e : {WCon{b, x} == WCon{b, _} : Word(1n+p)}
403	  {==}
404	
405	def AP.u32_cong(-x: Word(32n), -y: Word(32n), e: {x == y : Word(32n)}) -> {U32{x} == U32{y} : U32}:
406	  %e : {U32{x} == U32{_} : U32}
407	  {==}
408	
409	# 2^d as a word, and the mask of the low d bits
410	
411	def AP.pw(n: Nat, d: Nat) -> Word(n):
412	  match n:
413	    case 0n:
414	      WNil{}
415	    case 1n+q:
416	      match d:
417	        case 0n:
418	          WCon{True{}, Word.zero(q)}
419	        case 1n+e:
420	          WCon{False{}, AP.pw(q, e)}
421	
422	def AP.lm(n: Nat, d: Nat) -> Word(n):
423	  match n:
424	    case 0n:
425	      WNil{}
426	    case 1n+q:
427	      match d:
428	        case 0n:
429	          WCon{False{}, Word.zero(q)}
430	        case 1n+e:
431	          WCon{True{}, AP.lm(q, e)}
432	
433	def AP.spzz(n: Nat) -> {Word.shl.put(n, False{}, Word.zero(n)) == Word.zero(n) : Word(n)}:
434	  match n:
435	    case 0n:
436	      {==}
437	    case 1n+ +q:
438	      AP.wcon_cong(q, False{}, Word.shl.put(q, False{}, Word.zero(q)), Word.zero(q), AP.spzz(q))
439	
440	def AP.spz(n: Nat) -> {Word.shl.put(n, True{}, Word.zero(n)) == AP.pw(n, 0n) : Word(n)}:
441	  match n:
442	    case 0n:
443	      {==}
444	    case 1n+ +q:
445	      AP.wcon_cong(q, True{}, Word.shl.put(q, False{}, Word.zero(q)), Word.zero(q), AP.spzz(q))
446	
447	def AP.sp(n: Nat, d: Nat) -> {Word.shl.put(n, False{}, AP.pw(n, d)) == AP.pw(n, 1n+d) : Word(n)}:
448	  match n:
449	    case 0n:
450	      {==}
451	    case 1n+ +q:
452	      match d:
453	        case 0n:
454	          AP.wcon_cong(q, False{}, Word.shl.put(q, True{}, Word.zero(q)), AP.pw(q, 0n), AP.spz(q))
455	        case 1n+ +e:
456	          AP.wcon_cong(q, False{}, Word.shl.put(q, False{}, AP.pw(q, e)), AP.pw(q, 1n+e), AP.sp(q, e))
457	
458	def AP.shl_put(n: Nat, w: Word(n)) -> {Word.shl(n, w) == Word.shl.put(n, False{}, w) : Word(n)}:
459	  match n:
460	    case 0n:
461	      {==}
462	    case 1n+q:
463	      match w:
464	        case WCon{b, t}:
465	          {==}
466	
467	# shln(1, d) is 2^d
468	def AP.shln_pw(d: Nat) -> {U32.shln(1, d) == U32{AP.pw(32n, d)} : U32}:
469	  match d:
470	    case 0n:
471	      {==}
472	    case 1n+ +e:
473	      %Equal.sym(U32, U32.shln(1, e), U32{AP.pw(32n, e)}, AP.shln_pw(e)) : {U32.shl(_) == U32{AP.pw(32n, 1n+e)} : U32}
474	      AP.u32_cong(Word.shl(32n, AP.pw(32n, e)), AP.pw(32n, 1n+e), Equal.trans(Word(32n), Word.shl(32n, AP.pw(32n, e)), Word.shl.put(32n, False{}, AP.pw(32n, e)), AP.pw(32n, 1n+e), AP.shl_put(32n, AP.pw(32n, e)), AP.sp(32n, e)))
475	
476	def AP.padz(n: Nat) -> {Word.shr.pad(n, Word.zero(n)) == Word.zero(1n+n) : Word(1n+n)}:
477	  match n:
478	    case 0n:
479	      {==}
480	    case 1n+ +q:
481	      AP.wcon_cong(1n+q, False{}, Word.shr.pad(q, Word.zero(q)), Word.zero(1n+q), AP.padz(q))
482	
483	def AP.padp(n: Nat, d: Nat, h: {Nat.is_lt(d, n) == True{} : Bool}) -> {Word.shr.pad(n, AP.pw(n, d)) == AP.pw(1n+n, d) : Word(1n+n)}:
484	  match n:
485	    case 0n:
486	      match d:
487	        case 0n:
488	          Empty.absurd({Word.shr.pad(0n, AP.pw(0n, 0n)) == AP.pw(1n, 0n) : Word(1n)}, AP.ft(h))
489	        case 1n+e:
490	          Empty.absurd({Word.shr.pad(0n, AP.pw(0n, 1n+e)) == AP.pw(1n, 1n+e) : Word(1n)}, AP.ft(h))
491	    case 1n+ +q:
492	      match d:
493	        case 0n:
494	          AP.wcon_cong(1n+q, True{}, Word.shr.pad(q, Word.zero(q)), Word.zero(1n+q), AP.padz(q))
495	        case 1n+ +e:
496	          AP.wcon_cong(1n+q, False{}, Word.shr.pad(q, AP.pw(q, e)), AP.pw(1n+q, e), AP.padp(q, e, h))
497	
498	def AP.shr_pw(n: Nat, d: Nat, h: {Nat.is_lt(1n+d, n) == True{} : Bool}) -> {Word.shr(n, AP.pw(n, 1n+d)) == AP.pw(n, d) : Word(n)}:
499	  match n:
500	    case 0n:
501	      Empty.absurd({Word.shr(0n, AP.pw(0n, 1n+d)) == AP.pw(0n, d) : Word(0n)}, AP.ft(h))
502	    case 1n+q:
503	      AP.padp(q, d, h)
504	
505	def AP.pw_shln(+d: Nat) -> {U32{AP.pw(32n, d)} == U32.shln(1, d) : U32}:
506	  Equal.sym(U32, U32.shln(1, d), U32{AP.pw(32n, d)}, AP.shln_pw(d))
507	
508	# halving 2^(d+1) gives 2^d (below 2^32)
509	def AP.shr_shln(+d: Nat, h: {Nat.is_lt(1n+d, 32n) == True{} : Bool}) -> {U32.shr(U32.shln(1, 1n+d)) == U32.shln(1, d) : U32}:
510	  %AP.pw_shln(1n+d) : {U32.shr(_) == U32.shln(1, d) : U32}
511	  %AP.pw_shln(d) : {U32.shr(U32{AP.pw(32n, 1n+d)}) == _ : U32}
512	  AP.u32_cong(Word.shr(32n, AP.pw(32n, 1n+d)), AP.pw(32n, d), AP.shr_pw(32n, d, h))
513	
514	# values
515	
516	def AP.val_zero(n: Nat) -> {Word.to_nat(n, Word.zero(n)) == 0n : Nat}:
517	  match n:
518	    case 0n:
519	      {==}
520	    case 1n+ +q:
521	      %Equal.sym(Nat, Word.to_nat(q, Word.zero(q)), 0n, AP.val_zero(q)) : {Nat.double(_) == 0n : Nat}
522	      {==}
523	
524	def AP.val_pw(n: Nat, d: Nat, h: {Nat.is_lt(d, n) == True{} : Bool}) -> {Word.to_nat(n, AP.pw(n, d)) == A.Arrays.slots(d) : Nat}:
525	  match n:
526	    case 0n:
527	      match d:
528	        case 0n:
529	          Empty.absurd({Word.to_nat(0n, AP.pw(0n, 0n)) == A.Arrays.slots(0n) : Nat}, AP.ft(h))
530	        case 1n+e:
531	          Empty.absurd({Word.to_nat(0n, AP.pw(0n, 1n+e)) == A.Arrays.slots(1n+e) : Nat}, AP.ft(h))
532	    case 1n+ +q:
533	      match d:
534	        case 0n:
535	          %Equal.sym(Nat, Word.to_nat(q, Word.zero(q)), 0n, AP.val_zero(q)) : {1n+Nat.double(_) == 1n : Nat}
536	          {==}
537	        case 1n+ +e:
538	          AP.double_cong(Word.to_nat(q, AP.pw(q, e)), A.Arrays.slots(e), AP.val_pw(q, e, h))
539	
540	def AP.val_shln(+d: Nat, h: {Nat.is_lt(d, 32n) == True{} : Bool}) -> {U32.to_nat(U32.shln(1, d)) == A.Arrays.slots(d) : Nat}:
541	  %AP.pw_shln(d) : {U32.to_nat(_) == A.Arrays.slots(d) : Nat}
542	  AP.val_pw(32n, d, h)
543	
544	# 2^d - 1 is the mask of the low d bits
545	
546	def AP.z1(n: Nat) -> {Word.adc(n, Word.zero(n), Word.zero(n), True{}, True{}) == Word.zero(n) : Word(n)}:
547	  match n:
548	    case 0n:
549	      {==}
550	    case 1n+ +q:
551	      AP.wcon_cong(q, False{}, Word.adc(q, Word.zero(q), Word.zero(q), True{}, True{}), Word.zero(q), AP.z1(q))
552	
553	def AP.z2(n: Nat, d: Nat) -> {Word.adc(n, AP.pw(n, d), Word.zero(n), True{}, False{}) == AP.lm(n, d) : Word(n)}:
554	  match n:
555	    case 0n:
556	      {==}
557	    case 1n+ +q:
558	      match d:
559	        case 0n:
560	          AP.wcon_cong(q, False{}, Word.adc(q, Word.zero(q), Word.zero(q), True{}, True{}), Word.zero(q), AP.z1(q))
561	        case 1n+ +e:
562	          AP.wcon_cong(q, True{}, Word.adc(q, AP.pw(q, e), Word.zero(q), True{}, False{}), AP.lm(q, e), AP.z2(q, e))
563	
564	def AP.sub_one(n: Nat, d: Nat) -> {Word.sub(n, AP.pw(n, d), AP.pw(n, 0n)) == AP.lm(n, d) : Word(n)}:
565	  match n:
566	    case 0n:
567	      {==}
568	    case 1n+ +q:
569	      match d:
570	        case 0n:
571	          AP.wcon_cong(q, False{}, Word.adc(q, Word.zero(q), Word.zero(q), True{}, True{}), Word.zero(q), AP.z1(q))
572	        case 1n+ +e:
573	          AP.wcon_cong(q, True{}, Word.adc(q, AP.pw(q, e), Word.zero(q), True{}, False{}), AP.lm(q, e), AP.z2(q, e))
574	
575	def AP.mask_lm(+d: Nat) -> {U32.sub(U32.shln(1, d), 1) == U32{AP.lm(32n, d)} : U32}:
576	  %AP.pw_shln(d) : {U32.sub(_, 1) == U32{AP.lm(32n, d)} : U32}
577	  AP.u32_cong(Word.sub(32n, AP.pw(32n, d), AP.pw(32n, 0n)), AP.lm(32n, d), AP.sub_one(32n, d))
578	
579	
580	# A Data mirror of an array, so that lemmas can mention one array many times
581	
582	type AP.Tree<-T: Data> is Data:
583	  APLeaf{value: T}
584	  APNode{xs: AP.Tree<T>, ys: AP.Tree<T>}
585	
586	def AP.build(-T: Data, t: AP.Tree<T>) -> Array<T>:
587	  match t:
588	    case APLeaf{x}:
589	      ALeaf{x}
590	    case APNode{xs, ys}:
591	      ANode{AP.build(T, xs), AP.build(T, ys)}
592	
593	def AP.reflect.node(-T: Data, -tx: AP.Tree<T>, -ty: AP.Tree<T>, -xs: Array<T>, -ys: Array<T>, ex: {AP.build(T, tx) == xs : Array<T>}, ey: {AP.build(T, ty) == ys : Array<T>}) -> {ANode{AP.build(T, tx), AP.build(T, ty)} == ANode{xs, ys} : Array<T>}:
594	  %ex : {ANode{AP.build(T, tx), AP.build(T, ty)} == ANode{_, ys} : Array<T>}
595	  %ey : {ANode{AP.build(T, tx), AP.build(T, ty)} == ANode{AP.build(T, tx), _} : Array<T>}
596	  {==}
597	
598	def AP.reflect.join(-T: Data, -xs: Array<T>, -ys: Array<T>, rx: &t: AP.Tree<T> -> {AP.build(T, t) == xs : Array<T>}, ry: &t: AP.Tree<T> -> {AP.build(T, t) == ys : Array<T>}) -> &t: AP.Tree<T> -> {AP.build(T, t) == ANode{xs, ys} : Array<T>}:
599	  (tx, ex) = rx
600	  (ty, ey) = ry
601	  (APNode{tx, ty}, AP.reflect.node(T, tx, ty, xs, ys, ex, ey))
602	
603	def AP.reflect(-T: Data, a: Array<T>) -> &t: AP.Tree<T> -> {AP.build(T, t) == a : Array<T>}:
604	  match a:
605	    case ALeaf{x}:
606	      (APLeaf{x}, {==})
607	    case ANode{xs, ys}:
608	      AP.reflect.join(T, xs, ys, AP.reflect(T, xs), AP.reflect(T, ys))
609	
610	# Bool facts
611	
612	def AP.and_l(a: Bool, -b: Bool, e: {Bool.and(a, b) == True{} : Bool}) -> {a == True{} : Bool}:
613	  match a:
614	    case True{}:
615	      {==}
616	    case False{}:
617	      Empty.absurd({False{} == True{} : Bool}, AP.ft(e))
618	
619	def AP.and_r(a: Bool, -b: Bool, e: {Bool.and(a, b) == True{} : Bool}) -> {b == True{} : Bool}:
620	  match a:
621	    case True{}:
622	      e
623	    case False{}:
624	      Empty.absurd({b == True{} : Bool}, AP.ft(e))
625	
626	# The mirror of Base's array code on the Data tree: the same index
627	# arithmetic, so each lemma below is a plain induction
628	
629	def AP.size(-T: Data, t: AP.Tree<T>) -> U32:
630	  match t:
631	    case APLeaf{x}:
632	      1
633	    case APNode{xs, ys}:
634	      U32.shl(AP.size(T, xs))
635	
636	def AP.swap_t(-T: Data, t: AP.Tree<T>, n: U32, +i: U32, v: T, z: Bool) -> AP.Tree<T>:
637	  match t z:
638	    case APLeaf{x} _:
639	      APLeaf{v}
640	    case APNode{xs, ys} True{}:
641	      +h = U32.shr(n)
642	      APNode{AP.swap_t(T, xs, h, i, v, U32.is_lt(i, U32.shr(h))), ys}
643	    case APNode{xs, ys} False{}:
644	      +h = U32.shr(n)
645	      +j = U32.sub(i, h)
646	      APNode{xs, AP.swap_t(T, ys, h, j, v, U32.is_lt(j, U32.shr(h)))}
647	
648	def AP.swap_v(-T: Data, t: AP.Tree<T>, n: U32, +i: U32, v: T, z: Bool) -> T:
649	  match t z:
650	    case APLeaf{x} _:
651	      x
652	    case APNode{xs, ys} True{}:
653	      +h = U32.shr(n)
654	      AP.swap_v(T, xs, h, i, v, U32.is_lt(i, U32.shr(h)))
655	    case APNode{xs, ys} False{}:
656	      +h = U32.shr(n)
657	      +j = U32.sub(i, h)
658	      AP.swap_v(T, ys, h, j, v, U32.is_lt(j, U32.shr(h)))
659	
660	def AP.get_v(-T: Data, t: AP.Tree<T>, n: U32, +i: U32, z: Bool) -> T:
661	  match t z:
662	    case APLeaf{x} _:
663	      x
664	    case APNode{xs, ys} True{}:
665	      +h = U32.shr(n)
666	      AP.get_v(T, xs, h, i, U32.is_lt(i, U32.shr(h)))
667	    case APNode{xs, ys} False{}:
668	      +h = U32.shr(n)
669	      +j = U32.sub(i, h)
670	      AP.get_v(T, ys, h, j, U32.is_lt(j, U32.shr(h)))
671	
672	def AP.mask(+n: U32, i: U32) -> U32:
673	  U32.and(i, U32.sub(n, 1))
674	
675	def AP.z(+n: U32, +j: U32) -> Bool:
676	  U32.is_lt(j, U32.shr(n))
677	
678	def AP.get_top(-T: Data, +t: AP.Tree<T>, i: U32) -> T:
679	  +n = AP.size(T, t)
680	  +j = AP.mask(n, i)
681	  AP.get_v(T, t, n, j, AP.z(n, j))
682	
683	def AP.set_top(-T: Data, +t: AP.Tree<T>, i: U32, v: T) -> AP.Tree<T>:
684	  +n = AP.size(T, t)
685	  +j = AP.mask(n, i)
686	  AP.swap_t(T, t, n, j, v, AP.z(n, j))
687	
688	# Base's code on a built tree is the mirror
689	
690	def AP.size_eq(-T: Data, t: AP.Tree<T>) -> {Array.size(T, AP.build(T, t)) == (AP.build(T, t), AP.size(T, t)) : Array<T> & U32}:
691	  match t:
692	    case APLeaf{x}:
693	      {==}
694	    case APNode{xs, ys}:
695	      %Equal.sym(Array<T> & U32, Array.size(T, AP.build(T, xs)), (AP.build(T, xs), AP.size(T, xs)), AP.size_eq(T, xs)) : {Array.size.node(T, AP.build(T, ys), _) == (ANode{AP.build(T, xs), AP.build(T, ys)}, U32.shl(AP.size(T, xs))) : Array<T> & U32}
696	      {==}
697	
698	def AP.swap_eq(-T: Data, t: AP.Tree<T>, n: U32, +i: U32, v: T, z: Bool) -> {Array.swap.go(T, AP.build(T, t), n, i, v, z) == (AP.build(T, AP.swap_t(T, t, n, i, v, z)), AP.swap_v(T, t, n, i, v, z)) : Array<T> & T}:
699	  match t z:
700	    case APLeaf{x} _:
701	      {==}
702	    case APNode{xs, ys} True{}:
703	      +h = U32.shr(n)
704	      +z1 = U32.is_lt(i, U32.shr(h))
705	      %Equal.sym(Array<T> & T, Array.swap.go(T, AP.build(T, xs), h, i, v, z1), (AP.build(T, AP.swap_t(T, xs, h, i, v, z1)), AP.swap_v(T, xs, h, i, v, z1)), AP.swap_eq(T, xs, h, i, v, z1)) : {Array.swap.lo(T, AP.build(T, ys), _) == (ANode{AP.build(T, AP.swap_t(T, xs, h, i, v, z1)), AP.build(T, ys)}, AP.swap_v(T, xs, h, i, v, z1)) : Array<T> & T}
706	      {==}
707	    case APNode{xs, ys} False{}:
708	      +h = U32.shr(n)
709	      +j = U32.sub(i, h)
710	      +z1 = U32.is_lt(j, U32.shr(h))
711	      %Equal.sym(Array<T> & T, Array.swap.go(T, AP.build(T, ys), h, j, v, z1), (AP.build(T, AP.swap_t(T, ys, h, j, v, z1)), AP.swap_v(T, ys, h, j, v, z1)), AP.swap_eq(T, ys, h, j, v, z1)) : {Array.swap.hi(T, AP.build(T, xs), _) == (ANode{AP.build(T, xs), AP.build(T, AP.swap_t(T, ys, h, j, v, z1))}, AP.swap_v(T, ys, h, j, v, z1)) : Array<T> & T}
712	      {==}
713	
714	def AP.get_eq(-T: Data, t: AP.Tree<T>, n: U32, +i: U32, z: Bool) -> {Array.get.go(T, AP.build(T, t), n, i, z) == (AP.build(T, t), AP.get_v(T, t, n, i, z)) : Array<T> & T}:
715	  match t z:
716	    case APLeaf{x} _:
717	      {==}
718	    case APNode{xs, ys} True{}:
719	      +h = U32.shr(n)
720	      +z1 = U32.is_lt(i, U32.shr(h))
721	      %Equal.sym(Array<T> & T, Array.get.go(T, AP.build(T, xs), h, i, z1), (AP.build(T, xs), AP.get_v(T, xs, h, i, z1)), AP.get_eq(T, xs, h, i, z1)) : {Array.swap.lo(T, AP.build(T, ys), _) == (ANode{AP.build(T, xs), AP.build(T, ys)}, AP.get_v(T, xs, h, i, z1)) : Array<T> & T}
722	      {==}
723	    case APNode{xs, ys} False{}:
724	      +h = U32.shr(n)
725	      +j = U32.sub(i, h)
726	      +z1 = U32.is_lt(j, U32.shr(h))
727	      %Equal.sym(Array<T> & T, Array.get.go(T, AP.build(T, ys), h, j, z1), (AP.build(T, ys), AP.get_v(T, ys, h, j, z1)), AP.get_eq(T, ys, h, j, z1)) : {Array.swap.hi(T, AP.build(T, xs), _) == (ANode{AP.build(T, xs), AP.build(T, ys)}, AP.get_v(T, ys, h, j, z1)) : Array<T> & T}
728	      {==}
729	
730	def AP.get_top_eq(-T: Data, +t: AP.Tree<T>, +i: U32) -> {Array.get(T, AP.build(T, t), i) == (AP.build(T, t), AP.get_top(T, t, i)) : Array<T> & T}:
731	  +n = AP.size(T, t)
732	  +j = AP.mask(n, i)
733	  %Equal.sym(Array<T> & U32, Array.size(T, AP.build(T, t)), (AP.build(T, t), n), AP.size_eq(T, t)) : {Array.get.at(T, i, _) == (AP.build(T, t), AP.get_top(T, t, i)) : Array<T> & T}
734	  %Equal.sym(Array<T> & T, Array.get.go(T, AP.build(T, t), n, j, AP.z(n, j)), (AP.build(T, t), AP.get_v(T, t, n, j, AP.z(n, j))), AP.get_eq(T, t, n, j, AP.z(n, j))) : {_ == (AP.build(T, t), AP.get_top(T, t, i)) : Array<T> & T}
735	  {==}
736	
737	def AP.set_top_eq(-T: Data, +t: AP.Tree<T>, +i: U32, +v: T) -> {Array.set(T, AP.build(T, t), i, v) == AP.build(T, AP.set_top(T, t, i, v)) : Array<T>}:
738	  +n = AP.size(T, t)
739	  +j = AP.mask(n, i)
740	  %Equal.sym(Array<T> & U32, Array.size(T, AP.build(T, t)), (AP.build(T, t), n), AP.size_eq(T, t)) : {Array.set.fin(T, Array.swap.at(T, i, v, _)) == AP.build(T, AP.set_top(T, t, i, v)) : Array<T>}
741	  %Equal.sym(Array<T> & T, Array.swap.go(T, AP.build(T, t), n, j, v, AP.z(n, j)), (AP.build(T, AP.swap_t(T, t, n, j, v, AP.z(n, j))), AP.swap_v(T, t, n, j, v, AP.z(n, j))), AP.swap_eq(T, t, n, j, v, AP.z(n, j))) : {Array.set.fin(T, _) == AP.build(T, AP.set_top(T, t, i, v)) : Array<T>}
742	  {==}
743	
744	# Shape: a write replaces one leaf and keeps the shape
745	
746	def AP.swap_size(-T: Data, t: AP.Tree<T>, n: U32, +i: U32, v: T, z: Bool) -> {AP.size(T, AP.swap_t(T, t, n, i, v, z)) == AP.size(T, t) : U32}:
747	  match t z:
748	    case APLeaf{x} _:
749	      {==}
750	    case APNode{xs, ys} True{}:
751	      +h = U32.shr(n)
752	      +z1 = U32.is_lt(i, U32.shr(h))
753	      %Equal.sym(U32, AP.size(T, AP.swap_t(T, xs, h, i, v, z1)), AP.size(T, xs), AP.swap_size(T, xs, h, i, v, z1)) : {U32.shl(_) == U32.shl(AP.size(T, xs)) : U32}
754	      {==}
755	    case APNode{xs, ys} False{}:
756	      {==}
757	
758	def AP.get_swap_same(-T: Data, t: AP.Tree<T>, n: U32, +i: U32, +v: T, z: Bool) -> {AP.get_v(T, AP.swap_t(T, t, n, i, v, z), n, i, z) == v : T}:
759	  match t z:
760	    case APLeaf{x} _:
761	      {==}
762	    case APNode{xs, ys} True{}:
763	      +h = U32.shr(n)
764	      AP.get_swap_same(T, xs, h, i, v, U32.is_lt(i, U32.shr(h)))
765	    case APNode{xs, ys} False{}:
766	      +h = U32.shr(n)
767	      +j = U32.sub(i, h)
768	      AP.get_swap_same(T, ys, h, j, v, U32.is_lt(j, U32.shr(h)))
769	
770	def AP.perf_swap(-T: Data, t: AP.Tree<T>, n: U32, +i: U32, v: T, z: Bool, +d: Nat) -> {A.Arrays.is_perfect(T, d, AP.build(T, AP.swap_t(T, t, n, i, v, z))) == A.Arrays.is_perfect(T, d, AP.build(T, t)) : Bool}:
771	  match t z:
772	    case APLeaf{x} _:
773	      match d:
774	        case 0n:
775	          {==}
776	        case 1n+p:
777	          {==}
778	    case APNode{xs, ys} True{}:
779	      match d:
780	        case 0n:
781	          {==}
782	        case 1n+p:
783	          +h = U32.shr(n)
784	          +z1 = U32.is_lt(i, U32.shr(h))
785	          %Equal.sym(Bool, A.Arrays.is_perfect(T, p, AP.build(T, AP.swap_t(T, xs, h, i, v, z1))), A.Arrays.is_perfect(T, p, AP.build(T, xs)), AP.perf_swap(T, xs, h, i, v, z1, p)) : {Bool.and(_, A.Arrays.is_perfect(T, p, AP.build(T, ys))) == Bool.and(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys))) : Bool}
786	          {==}
787	    case APNode{xs, ys} False{}:
788	      match d:
789	        case 0n:
790	          {==}
791	        case 1n+p:
792	          +h = U32.shr(n)
793	          +j = U32.sub(i, h)
794	          +z1 = U32.is_lt(j, U32.shr(h))
795	          %Equal.sym(Bool, A.Arrays.is_perfect(T, p, AP.build(T, AP.swap_t(T, ys, h, j, v, z1))), A.Arrays.is_perfect(T, p, AP.build(T, ys)), AP.perf_swap(T, ys, h, j, v, z1, p)) : {Bool.and(A.Arrays.is_perfect(T, p, AP.build(T, xs)), _) == Bool.and(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys))) : Bool}
796	          {==}
797	
798	def AP.size_perf(-T: Data, +d: Nat, +t: AP.Tree<T>, h: {A.Arrays.is_perfect(T, d, AP.build(T, t)) == True{} : Bool}) -> {AP.size(T, t) == U32.shln(1, d) : U32}:
799	  match d t:
800	    case 0n APLeaf{x}:
801	      {==}
802	    case 0n APNode{xs, ys}:
803	      Empty.absurd({AP.size(T, APNode{xs, ys}) == U32.shln(1, 0n) : U32}, AP.ft(h))
804	    case 1n+p APLeaf{x}:
805	      Empty.absurd({AP.size(T, APLeaf{x}) == U32.shln(1, 1n+p) : U32}, AP.ft(h))
806	    case 1n+p APNode{xs, ys}:
807	      +hx = AP.and_l(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), h)
808	      %Equal.sym(U32, AP.size(T, xs), U32.shln(1, p), AP.size_perf(T, p, xs, hx)) : {U32.shl(_) == U32.shl(U32.shln(1, p)) : U32}
809	      {==}
810	
811	def AP.new_perf(-T: Data, +d: Nat, +v: T) -> {A.Arrays.is_perfect(T, d, Array.new(T, d, v)) == True{} : Bool}:
812	  match d:
813	    case 0n:
814	      {==}
815	    case 1n+p:
816	      %Equal.sym(Bool, A.Arrays.is_perfect(T, p, Array.new(T, p, v)), True{}, AP.new_perf(T, p, v)) : {Bool.and(_, _) == True{} : Bool}
817	      {==}
818	
819	# Reflected forms of the laws for every array
820	
821	def AP.get_same_array.go(-T: Data, -a: Array<T>, +i: U32, r: &t: AP.Tree<T> -> {AP.build(T, t) == a : Array<T>}) -> {Pair.fst(Array<T>, T, Array.get(T, a, i)) == a : Array<T>}:
822	  (t, e) = r
823	  %e : {Pair.fst(Array<T>, T, Array.get(T, _, i)) == _ : Array<T>}
824	  %Equal.sym(Array<T> & T, Array.get(T, AP.build(T, t), i), (AP.build(T, t), AP.get_top(T, t, i)), AP.get_top_eq(T, t, i)) : {Pair.fst(Array<T>, T, _) == AP.build(T, t) : Array<T>}
825	  {==}
826	
827	def AP.get_set_same.go(-T: Data, -a: Array<T>, +i: U32, +v: T, r: &t: AP.Tree<T> -> {AP.build(T, t) == a : Array<T>}) -> {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, a, i, v), i)) == v : T}:
828	  (+t, e) = r
829	  +n = AP.size(T, t)
830	  +j = AP.mask(n, i)
831	  +t2 = AP.set_top(T, t, i, v)
832	  %e : {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, _, i, v), i)) == v : T}
833	  %Equal.sym(Array<T>, Array.set(T, AP.build(T, t), i, v), AP.build(T, t2), AP.set_top_eq(T, t, i, v)) : {Pair.snd(Array<T>, T, Array.get(T, _, i)) == v : T}
834	  %Equal.sym(Array<T> & T, Array.get(T, AP.build(T, t2), i), (AP.build(T, t2), AP.get_top(T, t2, i)), AP.get_top_eq(T, t2, i)) : {Pair.snd(Array<T>, T, _) == v : T}
835	  %Equal.sym(U32, AP.size(T, t2), n, AP.swap_size(T, t, n, j, v, AP.z(n, j))) : {AP.get_v(T, t2, _, AP.mask(_, i), AP.z(_, AP.mask(_, i))) == v : T}
836	  AP.get_swap_same(T, t, n, j, v, AP.z(n, j))
837	
838	# More Nat order facts
839	
840	def AP.lt_zero(x: Nat) -> {Nat.is_lt(x, 0n) == False{} : Bool}:
841	  match x:
842	    case 0n:
843	      {==}
844	    case 1n+p:
845	      {==}
846	
847	def AP.lt_succ_l(x: Nat, y: Nat, h: {Nat.is_lt(1n+x, y) == True{} : Bool}) -> {Nat.is_lt(x, y) == True{} : Bool}:
848	  match x y:
849	    case 0n 0n:
850	      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, AP.ft(h))
851	    case 0n 1n+q:
852	      {==}
853	    case 1n+p 0n:
854	      Empty.absurd({Nat.is_lt(1n+p, 0n) == True{} : Bool}, AP.ft(h))
855	    case 1n+p 1n+q:
856	      AP.lt_succ_l(p, q, h)
857	
858	def AP.lt_le(x: Nat, y: Nat, h: {Nat.is_lt(x, y) == True{} : Bool}) -> {Nat.is_le(x, y) == True{} : Bool}:
859	  match x y:
860	    case 0n 0n:
861	      {==}
862	    case 0n 1n+q:
863	      {==}
864	    case 1n+p 0n:
865	      Empty.absurd({Nat.is_le(1n+p, 0n) == True{} : Bool}, AP.ft(h))
866	    case 1n+p 1n+q:
867	      AP.lt_le(p, q, h)
868	
869	def AP.lt_le_trans(a: Nat, b: Nat, k: Nat, h1: {Nat.is_lt(k, a) == True{} : Bool}, h2: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_lt(k, b) == True{} : Bool}:
870	  match a b:
871	    case 0n _:
872	      Empty.absurd({Nat.is_lt(k, b) == True{} : Bool}, AP.ft(Equal.trans(Bool, False{}, Nat.is_lt(k, 0n), True{}, Equal.sym(Bool, Nat.is_lt(k, 0n), False{}, AP.lt_zero(k)), h1)))
873	    case 1n+p 0n:
874	      Empty.absurd({Nat.is_lt(k, 0n) == True{} : Bool}, AP.ft(h2))
875	    case 1n+p 1n+q:
876	      match k:
877	        case 0n:
878	          {==}
879	        case 1n+r:
880	          AP.lt_le_trans(p, q, r, h1, h2)
881	
882	def AP.double_le(+x: Nat, +y: Nat, h: {Nat.is_le(x, y) == True{} : Bool}) -> {Nat.is_le(Nat.double(x), Nat.double(y)) == True{} : Bool}:
883	  %Equal.sym(Cmp, Nat.cmp(AP.bv(False{}, x), AP.bv(False{}, y)), Word.cmp.fin(False{}, False{}, Nat.cmp(x, y)), AP.nc(x, y, False{}, False{})) : {Cmp.is_le(_) == True{} : Bool}
884	  %Equal.sym(Bool, Cmp.is_le(Word.cmp.fin(False{}, False{}, Nat.cmp(x, y))), Cmp.is_le(Nat.cmp(x, y)), AP.fin_le_ff(Nat.cmp(x, y))) : {_ == True{} : Bool}
885	  h
886	
887	def AP.dpos(x: Nat, e: {Nat.is_lt(0n, x) == True{} : Bool}) -> {Nat.is_le(1n, Nat.double(x)) == True{} : Bool}:
888	  match x:
889	    case 0n:
890	      Empty.absurd({Nat.is_le(1n, 0n) == True{} : Bool}, AP.ft(e))
891	    case 1n+y:
892	      {==}
893	
894	def AP.slots_pos(d: Nat) -> {Nat.is_lt(0n, A.Arrays.slots(d)) == True{} : Bool}:
895	  match d:
896	    case 0n:
897	      {==}
898	    case 1n+ +p:
899	      AP.lt_le_trans(1n, Nat.double(A.Arrays.slots(p)), 0n, {==}, AP.dpos(A.Arrays.slots(p), AP.slots_pos(p)))
900	
901	def AP.slots_le(d: Nat, n: Nat, h: {Nat.is_le(d, n) == True{} : Bool}) -> {Nat.is_le(A.Arrays.slots(d), A.Arrays.slots(n)) == True{} : Bool}:
902	  match d n:
903	    case 0n 0n:
904	      {==}
905	    case 0n 1n+ +q:
906	      AP.dpos(A.Arrays.slots(q), AP.slots_pos(q))
907	    case 1n+p 0n:
908	      Empty.absurd({Nat.is_le(A.Arrays.slots(1n+p), A.Arrays.slots(0n)) == True{} : Bool}, AP.ft(h))
909	    case 1n+ +p 1n+ +q:
910	      AP.double_le(A.Arrays.slots(p), A.Arrays.slots(q), AP.slots_le(p, q, h))
911	
912	# a value below double(s), split at s
913	def AP.lt_split(+w: Nat, +s: Nat, h: {Nat.is_lt(Nat.add(w, s), Nat.double(s)) == True{} : Bool}) -> {Nat.is_lt(w, s) == True{} : Bool}:
914	  %AP.lt_cancel(s, w, s) : {_ == True{} : Bool}
915	  %AP.add_comm(w, s) : {Nat.is_lt(_, Nat.add(s, s)) == True{} : Bool}
916	  %AP.double_self(s) : {Nat.is_lt(Nat.add(w, s), _) == True{} : Bool}
917	  h
918	
919	# Lists
920	
921	def AP.con_cong(-T: Data, -h: T, -x: List<&2, T>, -y: List<&2, T>, e: {x == y : List<&2, T>}) -> {Con{h, x} == Con{h, y} : List<&2, T>}:
922	  %e : {Con{h, x} == Con{h, _} : List<&2, T>}
923	  {==}
924	
925	def AP.len_app(-T: Data, xs: List<&2, T>, -ys: List<&2, T>) -> {List.length(&2, T, List.append(&2, T, xs, ys)) == Nat.add(List.length(&2, T, xs), List.length(&2, T, ys)) : Nat}:
926	  match xs:
927	    case Nil{}:
928	      {==}
929	    case Con{h, t}:
930	      AP.succ_cong(List.length(&2, T, List.append(&2, T, t, ys)), Nat.add(List.length(&2, T, t), List.length(&2, T, ys)), AP.len_app(T, t, ys))
931	
932	def AP.get_app_l(-T: Data, xs: List<&2, T>, -ys: List<&2, T>, k: Nat, h: {Nat.is_lt(k, List.length(&2, T, xs)) == True{} : Bool}) -> {List.get(&2, T, List.append(&2, T, xs, ys), k) == List.get(&2, T, xs, k) : Maybe<&2, T>}:
933	  match xs k:
934	    case Nil{} _:
935	      Empty.absurd({List.get(&2, T, List.append(&2, T, Nil{}, ys), k) == List.get(&2, T, Nil{}, k) : Maybe<&2, T>}, AP.ft(Equal.trans(Bool, False{}, Nat.is_lt(k, 0n), True{}, Equal.sym(Bool, Nat.is_lt(k, 0n), False{}, AP.lt_zero(k)), h)))
936	    case Con{x, t} 0n:
937	      {==}
938	    case Con{x, t} 1n+p:
939	      AP.get_app_l(T, t, ys, p, h)
940	
941	def AP.get_app_r(-T: Data, xs: List<&2, T>, -ys: List<&2, T>, -k: Nat) -> {List.get(&2, T, List.append(&2, T, xs, ys), Nat.add(List.length(&2, T, xs), k)) == List.get(&2, T, ys, k) : Maybe<&2, T>}:
942	  match xs:
943	    case Nil{}:
944	      {==}
945	    case Con{x, t}:
946	      AP.get_app_r(T, t, ys, k)
947	
948	def AP.set_app_l(-T: Data, xs: List<&2, T>, -ys: List<&2, T>, k: Nat, -v: T, h: {Nat.is_lt(k, List.length(&2, T, xs)) == True{} : Bool}) -> {List.set(&2, T, List.append(&2, T, xs, ys), k, v) == List.append(&2, T, List.set(&2, T, xs, k, v), ys) : List<&2, T>}:
949	  match xs k:
950	    case Nil{} _:
951	      Empty.absurd({List.set(&2, T, List.append(&2, T, Nil{}, ys), k, v) == List.append(&2, T, List.set(&2, T, Nil{}, k, v), ys) : List<&2, T>}, AP.ft(Equal.trans(Bool, False{}, Nat.is_lt(k, 0n), True{}, Equal.sym(Bool, Nat.is_lt(k, 0n), False{}, AP.lt_zero(k)), h)))
952	    case Con{x, t} 0n:
953	      {==}
954	    case Con{x, t} 1n+p:
955	      AP.con_cong(T, x, List.set(&2, T, List.append(&2, T, t, ys), p, v), List.append(&2, T, List.set(&2, T, t, p, v), ys), AP.set_app_l(T, t, ys, p, v, h))
956	
957	def AP.set_app_r(-T: Data, xs: List<&2, T>, -ys: List<&2, T>, -k: Nat, -v: T) -> {List.set(&2, T, List.append(&2, T, xs, ys), Nat.add(List.length(&2, T, xs), k), v) == List.append(&2, T, xs, List.set(&2, T, ys, k, v)) : List<&2, T>}:
958	  match xs:
959	    case Nil{}:
960	      {==}
961	    case Con{x, t}:
962	      AP.con_cong(T, x, List.set(&2, T, List.append(&2, T, t, ys), Nat.add(List.length(&2, T, t), k), v), List.append(&2, T, t, List.set(&2, T, ys, k, v)), AP.set_app_r(T, t, ys, k, v))
963	
964	def AP.get_set_other(-T: Data, xs: List<&2, T>, k1: Nat, k2: Nat, -v: T, h: {Nat.is_eq(k1, k2) == False{} : Bool}) -> {List.get(&2, T, List.set(&2, T, xs, k1, v), k2) == List.get(&2, T, xs, k2) : Maybe<&2, T>}:
965	  match xs k1 k2:
966	    case Nil{} _ _:
967	      {==}
968	    case Con{x, t} 0n 0n:
969	      Empty.absurd({List.get(&2, T, List.set(&2, T, Con{x, t}, 0n, v), 0n) == List.get(&2, T, Con{x, t}, 0n) : Maybe<&2, T>}, AP.tf(h))
970	    case Con{x, t} 0n 1n+q:
971	      {==}
972	    case Con{x, t} 1n+p 0n:
973	      {==}
974	    case Con{x, t} 1n+p 1n+q:
975	      AP.get_set_other(T, t, p, q, v, h)
976	
977	# Masks and words below 2^d
978	
979	def AP.and_zero(n: Nat, w: Word(n)) -> {Word.and(n, w, Word.zero(n)) == Word.zero(n) : Word(n)}:
980	  match n:
981	    case 0n:
982	      {==}
983	    case 1n+ +q:
984	      match w:
985	        case WCon{False{}, t}:
986	          AP.wcon_cong(q, False{}, Word.and(q, t, Word.zero(q)), Word.zero(q), AP.and_zero(q, t))
987	        case WCon{True{}, t}:
988	          AP.wcon_cong(q, False{}, Word.and(q, t, Word.zero(q)), Word.zero(q), AP.and_zero(q, t))
989	
990	def AP.val0(n: Nat, w: Word(n), e: {Word.to_nat(n, w) == 0n : Nat}) -> {w == Word.zero(n) : Word(n)}:
991	  match n:
992	    case 0n:
993	      match w:
994	        case WNil{}:
995	          {==}
996	    case 1n+ +q:
997	      match w:
998	        case WCon{False{}, +t}:
999	          AP.wcon_cong(q, False{}, t, Word.zero(q), AP.val0(q, t, AP.double_zero(Word.to_nat(q, t), e)))
1000	        case WCon{True{}, +t}:
1001	          Empty.absurd({WCon{True{}, t} == Word.zero(1n+q) : Word(1n+q)}, AP.sz(Nat.double(Word.to_nat(q, t)), e))
1002	
1003	def AP.lt_bv_inv(+b: Bool, +x: Nat, +s: Nat, h: {Nat.is_lt(AP.bv(b, x), AP.bv(False{}, s)) == True{} : Bool}) -> {Nat.is_lt(x, s) == True{} : Bool}:
1004	  %AP.fin_lt_xf(b, Nat.cmp(x, s)) : {_ == True{} : Bool}
1005	  AP.lt_bits(x, s, b, False{}, h)
1006	
1007	def AP.lt_bv(+b: Bool, +x: Nat, +s: Nat, h: {Nat.is_lt(x, s) == True{} : Bool}) -> {Nat.is_lt(AP.bv(b, x), AP.bv(False{}, s)) == True{} : Bool}:
1008	  %Equal.sym(Cmp, Nat.cmp(AP.bv(b, x), AP.bv(False{}, s)), Word.cmp.fin(b, False{}, Nat.cmp(x, s)), AP.nc(x, s, b, False{})) : {Cmp.is_lt(_) == True{} : Bool}
1009	  %Equal.sym(Bool, Cmp.is_lt(Word.cmp.fin(b, False{}, Nat.cmp(x, s))), Cmp.is_lt(Nat.cmp(x, s)), AP.fin_lt_xf(b, Nat.cmp(x, s))) : {_ == True{} : Bool}
1010	  h
1011	
1012	# a word masked to its low d bits is below 2^d
1013	def AP.mask_lt(n: Nat, w: Word(n), +d: Nat) -> {Nat.is_lt(Word.to_nat(n, Word.and(n, w, AP.lm(n, d))), A.Arrays.slots(d)) == True{} : Bool}:
1014	  match n:
1015	    case 0n:
1016	      AP.slots_pos(d)
1017	    case 1n+ +q:
1018	      match w d:
1019	        case WCon{False{}, +t} 0n:
1020	          %Equal.sym(Word(q), Word.and(q, t, Word.zero(q)), Word.zero(q), AP.and_zero(q, t)) : {Nat.is_lt(Nat.double(Word.to_nat(q, _)), 1n) == True{} : Bool}
1021	          %Equal.sym(Nat, Word.to_nat(q, Word.zero(q)), 0n, AP.val_zero(q)) : {Nat.is_lt(Nat.double(_), 1n) == True{} : Bool}
1022	          {==}
1023	        case WCon{True{}, +t} 0n:
1024	          %Equal.sym(Word(q), Word.and(q, t, Word.zero(q)), Word.zero(q), AP.and_zero(q, t)) : {Nat.is_lt(Nat.double(Word.to_nat(q, _)), 1n) == True{} : Bool}
1025	          %Equal.sym(Nat, Word.to_nat(q, Word.zero(q)), 0n, AP.val_zero(q)) : {Nat.is_lt(Nat.double(_), 1n) == True{} : Bool}
1026	          {==}
1027	        case WCon{False{}, +t} 1n+ +e:
1028	          AP.lt_bv(False{}, Word.to_nat(q, Word.and(q, t, AP.lm(q, e))), A.Arrays.slots(e), AP.mask_lt(q, t, e))
1029	        case WCon{True{}, +t} 1n+ +e:
1030	          AP.lt_bv(True{}, Word.to_nat(q, Word.and(q, t, AP.lm(q, e))), A.Arrays.slots(e), AP.mask_lt(q, t, e))
1031	
1032	# a word below 2^d is unchanged by the mask
1033	def AP.and_id(n: Nat, w: Word(n), +d: Nat, h: {Nat.is_lt(Word.to_nat(n, w), A.Arrays.slots(d)) == True{} : Bool}) -> {Word.and(n, w, AP.lm(n, d)) == w : Word(n)}:
1034	  match n:
1035	    case 0n:
1036	      match w:
1037	        case WNil{}:
1038	          {==}
1039	    case 1n+ +q:
1040	      match w d:
1041	        case WCon{False{}, +t} 0n:
1042	          +z = AP.val0(q, t, AP.double_zero(Word.to_nat(q, t), AP.lt_one(Nat.double(Word.to_nat(q, t)), h)))
1043	          AP.wcon_cong(q, False{}, Word.and(q, t, Word.zero(q)), t, Equal.trans(Word(q), Word.and(q, t, Word.zero(q)), Word.zero(q), t, AP.and_zero(q, t), Equal.sym(Word(q), t, Word.zero(q), z)))
1044	        case WCon{True{}, +t} 0n:
1045	          Empty.absurd({Word.and(1n+q, WCon{True{}, t}, AP.lm(1n+q, 0n)) == WCon{True{}, t} : Word(1n+q)}, AP.tf(Equal.trans(Bool, True{}, Nat.is_lt(Nat.double(Word.to_nat(q, t)), 0n), False{}, Equal.sym(Bool, Nat.is_lt(Nat.double(Word.to_nat(q, t)), 0n), True{}, h), AP.lt_zero(Nat.double(Word.to_nat(q, t))))))
1046	        case WCon{False{}, +t} 1n+ +e:
1047	          AP.wcon_cong(q, False{}, Word.and(q, t, AP.lm(q, e)), t, AP.and_id(q, t, e, AP.lt_bv_inv(False{}, Word.to_nat(q, t), A.Arrays.slots(e), h)))
1048	        case WCon{True{}, +t} 1n+ +e:
1049	          AP.wcon_cong(q, True{}, Word.and(q, t, AP.lm(q, e)), t, AP.and_id(q, t, e, AP.lt_bv_inv(True{}, Word.to_nat(q, t), A.Arrays.slots(e), h)))
1050	
1051	def AP.u32_mask_lt(a: U32, +d: Nat) -> {Nat.is_lt(U32.to_nat(U32.and(a, U32{AP.lm(32n, d)})), A.Arrays.slots(d)) == True{} : Bool}:
1052	  match a:
1053	    case U32{w}:
1054	      AP.mask_lt(32n, w, d)
1055	
1056	def AP.u32_and_id(+a: U32, +d: Nat, h: {Nat.is_lt(U32.to_nat(a), A.Arrays.slots(d)) == True{} : Bool}) -> {U32.and(a, U32{AP.lm(32n, d)}) == a : U32}:
1057	  match a:
1058	    case U32{+w}:
1059	      AP.u32_cong(Word.and(32n, w, AP.lm(32n, d)), w, AP.and_id(32n, w, d, h))
1060	
1061	# from_nat and to_nat are inverse below 2^32
1062	
1063	def AP.inc(n: Nat, w: Word(n), d: Nat, h: {Nat.is_lt(1n+Word.to_nat(n, w), A.Arrays.slots(d)) == True{} : Bool}, hd: {Nat.is_le(d, n) == True{} : Bool}) -> {Word.to_nat(n, Word.inc(n, w)) == 1n+Word.to_nat(n, w) : Nat}:
1064	  match n:
1065	    case 0n:
1066	      match w d:
1067	        case WNil{} 0n:
1068	          Empty.absurd({0n == 1n : Nat}, AP.ft(h))
1069	        case WNil{} 1n+e:
1070	          Empty.absurd({0n == 1n : Nat}, AP.ft(hd))
1071	    case 1n+ +q:
1072	      match w d:
1073	        case WCon{False{}, t} _:
1074	          {==}
1075	        case WCon{True{}, +t} 0n:
1076	          Empty.absurd({Word.to_nat(1n+q, Word.inc(1n+q, WCon{True{}, t})) == 1n+Word.to_nat(1n+q, WCon{True{}, t}) : Nat}, AP.ft(h))
1077	        case WCon{True{}, +t} 1n+ +e:
1078	          +x = Word.to_nat(q, t)
1079	          %Equal.sym(Nat, Word.to_nat(q, Word.inc(q, t)), 1n+x, AP.inc(q, t, e, AP.lt_bv_inv(False{}, 1n+x, A.Arrays.slots(e), h), hd)) : {Nat.double(_) == 2n+Nat.double(x) : Nat}
1080	          {==}
1081	
1082	def AP.u32_inc(a: U32, d: Nat, h: {Nat.is_lt(1n+U32.to_nat(a), A.Arrays.slots(d)) == True{} : Bool}, hd: {Nat.is_le(d, 32n) == True{} : Bool}) -> {U32.to_nat(U32.inc(a)) == 1n+U32.to_nat(a) : Nat}:
1083	  match a:
1084	    case U32{w}:
1085	      AP.inc(32n, w, d, h, hd)
1086	
1087	def AP.lt_rw(-x: Nat, -y: Nat, -s: Nat, e: {x == y : Nat}, h: {Nat.is_lt(1n+y, s) == True{} : Bool}) -> {Nat.is_lt(1n+x, s) == True{} : Bool}:
1088	  %Equal.sym(Nat, x, y, e) : {Nat.is_lt(1n+_, s) == True{} : Bool}
1089	  h
1090	
1091	# from_nat then to_nat is the identity below 2^d, d <= 32
1092	def AP.from_nat(k: Nat, +d: Nat, +h: {Nat.is_lt(k, A.Arrays.slots(d)) == True{} : Bool}, +hd: {Nat.is_le(d, 32n) == True{} : Bool}) -> {U32.to_nat(U32.from_nat(k)) == k : Nat}:
1093	  match k:
1094	    case 0n:
1095	      {==}
1096	    case 1n+ +p:
1097	      +ih = AP.from_nat(p, d, AP.lt_succ_l(p, A.Arrays.slots(d), h), hd)
1098	      Equal.trans(Nat, U32.to_nat(U32.inc(U32.from_nat(p))), 1n+U32.to_nat(U32.from_nat(p)), 1n+p, AP.u32_inc(U32.from_nat(p), d, AP.lt_rw(U32.to_nat(U32.from_nat(p)), p, A.Arrays.slots(d), ih, h), hd), AP.succ_cong(U32.to_nat(U32.from_nat(p)), p, ih))
1099	
1100	# Reading and writing a perfect tree: the slot is the index's value
1101	
1102	def AP.app_cong_l(-T: Data, -x: List<&2, T>, -y: List<&2, T>, -ys: List<&2, T>, e: {x == y : List<&2, T>}) -> {List.append(&2, T, x, ys) == List.append(&2, T, y, ys) : List<&2, T>}:
1103	  %e : {List.append(&2, T, x, ys) == List.append(&2, T, _, ys) : List<&2, T>}
1104	  {==}
1105	
1106	def AP.app_cong_r(-T: Data, -xs: List<&2, T>, -x: List<&2, T>, -y: List<&2, T>, e: {x == y : List<&2, T>}) -> {List.append(&2, T, xs, x) == List.append(&2, T, xs, y) : List<&2, T>}:
1107	  %e : {List.append(&2, T, xs, x) == List.append(&2, T, xs, _) : List<&2, T>}
1108	  {==}
1109	
1110	def AP.lt_rw_r(-k: Nat, -x: Nat, -y: Nat, e: {x == y : Nat}, h: {Nat.is_lt(k, y) == True{} : Bool}) -> {Nat.is_lt(k, x) == True{} : Bool}:
1111	  %Equal.sym(Nat, x, y, e) : {Nat.is_lt(k, _) == True{} : Bool}
1112	  h
1113	
1114	def AP.lt_rw_l(-x: Nat, -y: Nat, -m: Nat, e: {x == y : Nat}, h: {Nat.is_lt(y, m) == True{} : Bool}) -> {Nat.is_lt(x, m) == True{} : Bool}:
1115	  %Equal.sym(Nat, x, y, e) : {Nat.is_lt(_, m) == True{} : Bool}
1116	  h
1117	
1118	def AP.lt_split2(+w: Nat, +s: Nat, h: {Nat.is_lt(Nat.add(s, w), Nat.double(s)) == True{} : Bool}) -> {Nat.is_lt(w, s) == True{} : Bool}:
1119	  %AP.lt_cancel(s, w, s) : {_ == True{} : Bool}
1120	  %AP.double_self(s) : {Nat.is_lt(Nat.add(s, w), _) == True{} : Bool}
1121	  h
1122	
1123	def AP.eb_fix(+i: U32, +p: Nat, +b: Bool, hd: {Nat.is_lt(1n+p, 32n) == True{} : Bool}, eb: {U32.is_lt(i, U32.shr(U32.shln(1, 1n+p))) == b : Bool}) -> {U32.is_lt(i, U32.shln(1, p)) == b : Bool}:
1124	  %AP.shr_shln(p, hd) : {U32.is_lt(i, _) == b : Bool}
1125	  eb
1126	
1127	def AP.lt_true(+i: U32, +p: Nat, hd: {Nat.is_lt(p, 32n) == True{} : Bool}, e: {U32.is_lt(i, U32.shln(1, p)) == True{} : Bool}) -> {Nat.is_lt(U32.to_nat(i), A.Arrays.slots(p)) == True{} : Bool}:
1128	  %AP.val_shln(p, hd) : {Nat.is_lt(U32.to_nat(i), _) == True{} : Bool}
1129	  %AP.u32_lt(i, U32.shln(1, p)) : {_ == True{} : Bool}
1130	  e
1131	
1132	def AP.lt_false(+i: U32, +p: Nat, hd: {Nat.is_lt(p, 32n) == True{} : Bool}, e: {U32.is_lt(i, U32.shln(1, p)) == False{} : Bool}) -> {Nat.is_lt(U32.to_nat(i), A.Arrays.slots(p)) == False{} : Bool}:
1133	  %AP.val_shln(p, hd) : {Nat.is_lt(U32.to_nat(i), _) == False{} : Bool}
1134	  %AP.u32_lt(i, U32.shln(1, p)) : {_ == False{} : Bool}
1135	  e
1136	
1137	def AP.u32_sub_add(a: U32, b: U32, h: {Nat.is_le(U32.to_nat(b), U32.to_nat(a)) == True{} : Bool}) -> {U32.to_nat(a) == Nat.add(U32.to_nat(U32.sub(a, b)), U32.to_nat(b)) : Nat}:
1138	  match a b:
1139	    case U32{x} U32{y}:
1140	      AP.adc(32n, x, y, True{}, h)
1141	
1142	def AP.le_rw_l(-x: Nat, -y: Nat, -m: Nat, e: {x == y : Nat}, h: {Nat.is_le(y, m) == True{} : Bool}) -> {Nat.is_le(x, m) == True{} : Bool}:
1143	  %Equal.sym(Nat, x, y, e) : {Nat.is_le(_, m) == True{} : Bool}
1144	  h
1145	
1146	# an index at or above 2^p, split into 2^p and the rest
1147	def AP.split(+i: U32, +p: Nat, +hd: {Nat.is_lt(p, 32n) == True{} : Bool}, e: {U32.is_lt(i, U32.shln(1, p)) == False{} : Bool}) -> {Nat.add(A.Arrays.slots(p), U32.to_nat(U32.sub(i, U32.shln(1, p)))) == U32.to_nat(i) : Nat}:
1148	  +s = A.Arrays.slots(p)
1149	  +w = U32.to_nat(U32.sub(i, U32.shln(1, p)))
1150	  +le = AP.le_rw_l(U32.to_nat(U32.shln(1, p)), s, U32.to_nat(i), AP.val_shln(p, hd), AP.not_lt_le(U32.to_nat(i), s, AP.lt_false(i, p, hd, e)))
1151	  %Equal.sym(Nat, U32.to_nat(i), Nat.add(w, U32.to_nat(U32.shln(1, p))), AP.u32_sub_add(i, U32.shln(1, p), le)) : {Nat.add(s, w) == _ : Nat}
1152	  %Equal.sym(Nat, U32.to_nat(U32.shln(1, p)), s, AP.val_shln(p, hd)) : {Nat.add(s, w) == Nat.add(w, _) : Nat}
1153	  AP.add_comm(s, w)
1154	
1155	def AP.len_perf(-T: Data, +d: Nat, +t: AP.Tree<T>, +hp: {A.Arrays.is_perfect(T, d, AP.build(T, t)) == True{} : Bool}) -> {List.length(&2, T, A.Arrays.leaves(T, AP.build(T, t))) == A.Arrays.slots(d) : Nat}:
1156	  match d t:
1157	    case 0n APLeaf{x}:
1158	      {==}
1159	    case 0n APNode{xs, ys}:
1160	      Empty.absurd({List.length(&2, T, A.Arrays.leaves(T, AP.build(T, APNode{xs, ys}))) == A.Arrays.slots(0n) : Nat}, AP.ft(hp))
1161	    case 1n+p APLeaf{x}:
1162	      Empty.absurd({List.length(&2, T, A.Arrays.leaves(T, AP.build(T, APLeaf{x}))) == A.Arrays.slots(1n+p) : Nat}, AP.ft(hp))
1163	    case 1n+ +p APNode{xs, ys}:
1164	      +lx = A.Arrays.leaves(T, AP.build(T, xs))
1165	      +ly = A.Arrays.leaves(T, AP.build(T, ys))
1166	      +s = A.Arrays.slots(p)
1167	      +hpx = AP.and_l(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp)
1168	      +hpy = AP.and_r(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp)
1169	      %Equal.sym(Nat, List.length(&2, T, List.append(&2, T, lx, ly)), Nat.add(List.length(&2, T, lx), List.length(&2, T, ly)), AP.len_app(T, lx, ly)) : {_ == Nat.double(s) : Nat}
1170	      %Equal.sym(Nat, List.length(&2, T, lx), s, AP.len_perf(T, p, xs, hpx)) : {Nat.add(_, List.length(&2, T, ly)) == Nat.double(s) : Nat}
1171	      %Equal.sym(Nat, List.length(&2, T, ly), s, AP.len_perf(T, p, ys, hpy)) : {Nat.add(s, _) == Nat.double(s) : Nat}
1172	      Equal.sym(Nat, Nat.double(s), Nat.add(s, s), AP.double_self(s))
1173	
1174	def AP.get_leaves(-T: Data, +d: Nat, +t: AP.Tree<T>, +i: U32, b: Bool, +eb: {U32.is_lt(i, U32.shr(U32.shln(1, d))) == b : Bool}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hp: {A.Arrays.is_perfect(T, d, AP.build(T, t)) == True{} : Bool}, +hi: {Nat.is_lt(U32.to_nat(i), A.Arrays.slots(d)) == True{} : Bool}) -> {List.get(&2, T, A.Arrays.leaves(T, AP.build(T, t)), U32.to_nat(i)) == Some{AP.get_v(T, t, U32.shln(1, d), i, b)} : Maybe<&2, T>}:
1175	  match d t b:
1176	    case 0n APLeaf{+x} _:
1177	      %Equal.sym(Nat, U32.to_nat(i), 0n, AP.lt_one(U32.to_nat(i), hi)) : {List.get(&2, T, Con{x, Nil{}}, _) == Some{x} : Maybe<&2, T>}
1178	      {==}
1179	    case 0n APNode{xs, ys} _:
1180	      Empty.absurd({List.get(&2, T, A.Arrays.leaves(T, AP.build(T, APNode{xs, ys})), U32.to_nat(i)) == Some{AP.get_v(T, APNode{xs, ys}, U32.shln(1, 0n), i, b)} : Maybe<&2, T>}, AP.ft(hp))
1181	    case 1n+p APLeaf{x} _:
1182	      Empty.absurd({List.get(&2, T, A.Arrays.leaves(T, AP.build(T, APLeaf{x})), U32.to_nat(i)) == Some{AP.get_v(T, APLeaf{x}, U32.shln(1, 1n+p), i, b)} : Maybe<&2, T>}, AP.ft(hp))
1183	    case 1n+ +p APNode{xs, ys} True{}:
1184	      +hd1 = AP.lt_succ_l(p, 32n, hd)
1185	      +s = A.Arrays.slots(p)
1186	      +sh = U32.shln(1, p)
1187	      +lx = A.Arrays.leaves(T, AP.build(T, xs))
1188	      +ly = A.Arrays.leaves(T, AP.build(T, ys))
1189	      +v = U32.to_nat(i)
1190	      +hpx = AP.and_l(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp)
1191	      +hi1 = AP.lt_true(i, p, hd1, AP.eb_fix(i, p, True{}, hd, eb))
1192	      +hl = AP.lt_rw_r(v, List.length(&2, T, lx), s, AP.len_perf(T, p, xs, hpx), hi1)
1193	      %Equal.sym(U32, U32.shr(U32.shln(1, 1n+p)), sh, AP.shr_shln(p, hd)) : {List.get(&2, T, List.append(&2, T, lx, ly), v) == Some{AP.get_v(T, xs, _, i, U32.is_lt(i, U32.shr(_)))} : Maybe<&2, T>}
1194	      Equal.trans(Maybe<&2, T>, List.get(&2, T, List.append(&2, T, lx, ly), v), List.get(&2, T, lx, v), Some{AP.get_v(T, xs, sh, i, U32.is_lt(i, U32.shr(sh)))}, AP.get_app_l(T, lx, ly, v, hl), AP.get_leaves(T, p, xs, i, U32.is_lt(i, U32.shr(sh)), {==}, hd1, hpx, hi1))
1195	    case 1n+ +p APNode{xs, ys} False{}:
1196	      +hd1 = AP.lt_succ_l(p, 32n, hd)
1197	      +s = A.Arrays.slots(p)
1198	      +sh = U32.shln(1, p)
1199	      +lx = A.Arrays.leaves(T, AP.build(T, xs))
1200	      +ly = A.Arrays.leaves(T, AP.build(T, ys))
1201	      +j = U32.sub(i, sh)
1202	      +w = U32.to_nat(j)
1203	      +hpx = AP.and_l(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp)
1204	      +hpy = AP.and_r(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp)
1205	      +hs = AP.split(i, p, hd1, AP.eb_fix(i, p, False{}, hd, eb))
1206	      +hj = AP.lt_split2(w, s, AP.lt_rw_l(Nat.add(s, w), U32.to_nat(i), Nat.double(s), hs, hi))
1207	      %Equal.sym(U32, U32.shr(U32.shln(1, 1n+p)), sh, AP.shr_shln(p, hd)) : {List.get(&2, T, List.append(&2, T, lx, ly), U32.to_nat(i)) == Some{AP.get_v(T, ys, _, U32.sub(i, _), U32.is_lt(U32.sub(i, _), U32.shr(_)))} : Maybe<&2, T>}
1208	      %hs : {List.get(&2, T, List.append(&2, T, lx, ly), _) == Some{AP.get_v(T, ys, sh, j, U32.is_lt(j, U32.shr(sh)))} : Maybe<&2, T>}
1209	      %AP.len_perf(T, p, xs, hpx) : {List.get(&2, T, List.append(&2, T, lx, ly), Nat.add(_, w)) == Some{AP.get_v(T, ys, sh, j, U32.is_lt(j, U32.shr(sh)))} : Maybe<&2, T>}
1210	      Equal.trans(Maybe<&2, T>, List.get(&2, T, List.append(&2, T, lx, ly), Nat.add(List.length(&2, T, lx), w)), List.get(&2, T, ly, w), Some{AP.get_v(T, ys, sh, j, U32.is_lt(j, U32.shr(sh)))}, AP.get_app_r(T, lx, ly, w), AP.get_leaves(T, p, ys, j, U32.is_lt(j, U32.shr(sh)), {==}, hd1, hpy, hj))
1211	
1212	def AP.set_leaves(-T: Data, +d: Nat, +t: AP.Tree<T>, +i: U32, +v: T, b: Bool, +eb: {U32.is_lt(i, U32.shr(U32.shln(1, d))) == b : Bool}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hp: {A.Arrays.is_perfect(T, d, AP.build(T, t)) == True{} : Bool}, +hi: {Nat.is_lt(U32.to_nat(i), A.Arrays.slots(d)) == True{} : Bool}) -> {A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, t, U32.shln(1, d), i, v, b))) == List.set(&2, T, A.Arrays.leaves(T, AP.build(T, t)), U32.to_nat(i), v) : List<&2, T>}:
1213	  match d t b:
1214	    case 0n APLeaf{+x} _:
1215	      %Equal.sym(Nat, U32.to_nat(i), 0n, AP.lt_one(U32.to_nat(i), hi)) : {Con{v, Nil{}} == List.set(&2, T, Con{x, Nil{}}, _, v) : List<&2, T>}
1216	      {==}
1217	    case 0n APNode{xs, ys} _:
1218	      Empty.absurd({A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, APNode{xs, ys}, U32.shln(1, 0n), i, v, b))) == List.set(&2, T, A.Arrays.leaves(T, AP.build(T, APNode{xs, ys})), U32.to_nat(i), v) : List<&2, T>}, AP.ft(hp))
1219	    case 1n+p APLeaf{x} _:
1220	      Empty.absurd({A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, APLeaf{x}, U32.shln(1, 1n+p), i, v, b))) == List.set(&2, T, A.Arrays.leaves(T, AP.build(T, APLeaf{x})), U32.to_nat(i), v) : List<&2, T>}, AP.ft(hp))
1221	    case 1n+ +p APNode{xs, ys} True{}:
1222	      +hd1 = AP.lt_succ_l(p, 32n, hd)
1223	      +s = A.Arrays.slots(p)
1224	      +sh = U32.shln(1, p)
1225	      +lx = A.Arrays.leaves(T, AP.build(T, xs))
1226	      +ly = A.Arrays.leaves(T, AP.build(T, ys))
1227	      +k = U32.to_nat(i)
1228	      +z1 = U32.is_lt(i, U32.shr(sh))
1229	      +hpx = AP.and_l(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp)
1230	      +hi1 = AP.lt_true(i, p, hd1, AP.eb_fix(i, p, True{}, hd, eb))
1231	      +hl = AP.lt_rw_r(k, List.length(&2, T, lx), s, AP.len_perf(T, p, xs, hpx), hi1)
1232	      %Equal.sym(U32, U32.shr(U32.shln(1, 1n+p)), sh, AP.shr_shln(p, hd)) : {List.append(&2, T, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, xs, _, i, v, U32.is_lt(i, U32.shr(_))))), ly) == List.set(&2, T, List.append(&2, T, lx, ly), k, v) : List<&2, T>}
1233	      Equal.trans(List<&2, T>, List.append(&2, T, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, xs, sh, i, v, z1))), ly), List.append(&2, T, List.set(&2, T, lx, k, v), ly), List.set(&2, T, List.append(&2, T, lx, ly), k, v), AP.app_cong_l(T, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, xs, sh, i, v, z1))), List.set(&2, T, lx, k, v), ly, AP.set_leaves(T, p, xs, i, v, z1, {==}, hd1, hpx, hi1)), Equal.sym(List<&2, T>, List.set(&2, T, List.append(&2, T, lx, ly), k, v), List.append(&2, T, List.set(&2, T, lx, k, v), ly), AP.set_app_l(T, lx, ly, k, v, hl)))
1234	    case 1n+ +p APNode{xs, ys} False{}:
1235	      +hd1 = AP.lt_succ_l(p, 32n, hd)
1236	      +s = A.Arrays.slots(p)
1237	      +sh = U32.shln(1, p)
1238	      +lx = A.Arrays.leaves(T, AP.build(T, xs))
1239	      +ly = A.Arrays.leaves(T, AP.build(T, ys))
1240	      +j = U32.sub(i, sh)
1241	      +w = U32.to_nat(j)
1242	      +z1 = U32.is_lt(j, U32.shr(sh))
1243	      +hpx = AP.and_l(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp)
1244	      +hpy = AP.and_r(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp)
1245	      +hs = AP.split(i, p, hd1, AP.eb_fix(i, p, False{}, hd, eb))
1246	      +hj = AP.lt_split2(w, s, AP.lt_rw_l(Nat.add(s, w), U32.to_nat(i), Nat.double(s), hs, hi))
1247	      %Equal.sym(U32, U32.shr(U32.shln(1, 1n+p)), sh, AP.shr_shln(p, hd)) : {List.append(&2, T, lx, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, ys, _, U32.sub(i, _), v, U32.is_lt(U32.sub(i, _), U32.shr(_)))))) == List.set(&2, T, List.append(&2, T, lx, ly), U32.to_nat(i), v) : List<&2, T>}
1248	      %hs : {List.append(&2, T, lx, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, ys, sh, j, v, z1)))) == List.set(&2, T, List.append(&2, T, lx, ly), _, v) : List<&2, T>}
1249	      %AP.len_perf(T, p, xs, hpx) : {List.append(&2, T, lx, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, ys, sh, j, v, z1)))) == List.set(&2, T, List.append(&2, T, lx, ly), Nat.add(_, w), v) : List<&2, T>}
1250	      Equal.trans(List<&2, T>, List.append(&2, T, lx, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, ys, sh, j, v, z1)))), List.append(&2, T, lx, List.set(&2, T, ly, w, v)), List.set(&2, T, List.append(&2, T, lx, ly), Nat.add(List.length(&2, T, lx), w), v), AP.app_cong_r(T, lx, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, ys, sh, j, v, z1))), List.set(&2, T, ly, w, v), AP.set_leaves(T, p, ys, j, v, z1, {==}, hd1, hpy, hj)), Equal.sym(List<&2, T>, List.set(&2, T, List.append(&2, T, lx, ly), Nat.add(List.length(&2, T, lx), w), v), List.append(&2, T, lx, List.set(&2, T, ly, w, v)), AP.set_app_r(T, lx, ly, w, v)))
1251	
1252	# Array.new on the mirror
1253	
1254	def AP.tnew(-T: Data, +d: Nat, +v: T) -> AP.Tree<T>:
1255	  match d:
1256	    case 0n:
1257	      APLeaf{v}
1258	    case 1n+p:
1259	      APNode{AP.tnew(T, p, v), AP.tnew(T, p, v)}
1260	
1261	def AP.new_eq(-T: Data, +d: Nat, +v: T) -> {Array.new(T, d, v) == AP.build(T, AP.tnew(T, d, v)) : Array<T>}:
1262	  match d:
1263	    case 0n:
1264	      {==}
1265	    case 1n+p:
1266	      %Equal.sym(Array<T>, Array.new(T, p, v), AP.build(T, AP.tnew(T, p, v)), AP.new_eq(T, p, v)) : {ANode{_, _} == ANode{AP.build(T, AP.tnew(T, p, v)), AP.build(T, AP.tnew(T, p, v))} : Array<T>}
1267	      {==}
1268	
1269	def AP.get_v_new(-T: Data, +d: Nat, +v: T, n: U32, +i: U32, z: Bool) -> {AP.get_v(T, AP.tnew(T, d, v), n, i, z) == v : T}:
1270	  match d z:
1271	    case 0n _:
1272	      {==}
1273	    case 1n+p True{}:
1274	      +h = U32.shr(n)
1275	      AP.get_v_new(T, p, v, h, i, U32.is_lt(i, U32.shr(h)))
1276	    case 1n+p False{}:
1277	      +h = U32.shr(n)
1278	      +j = U32.sub(i, h)
1279	      AP.get_v_new(T, p, v, h, j, U32.is_lt(j, U32.shr(h)))
1280	
1281	def AP.rep_add(-T: Data, a: Nat, -b: Nat, -v: T) -> {List.replicate(T, Nat.add(a, b), v) == List.append(&2, T, List.replicate(T, a, v), List.replicate(T, b, v)) : List<&2, T>}:
1282	  match a:
1283	    case 0n:
1284	      {==}
1285	    case 1n+p:
1286	      AP.con_cong(T, v, List.replicate(T, Nat.add(p, b), v), List.append(&2, T, List.replicate(T, p, v), List.replicate(T, b, v)), AP.rep_add(T, p, b, v))
1287	
1288	def AP.unsome(-T: Data, m: Maybe<&2, T>, x: T) -> T:
1289	  match m:
1290	    case Some{y}:
1291	      y
1292	    case None{}:
1293	      x
1294	
1295	def AP.some_inj(-T: Data, -x: T, -y: T, e: {Some{x} == Some{y} : Maybe<&2, T>}) -> {x == y : T}:
1296	  Equal.cong(Maybe<&2, T>, T, m => AP.unsome(T, m, x), Some{x}, Some{y}, e)
1297	
1298	def AP.perf_rw(-T: Data, -d: Nat, -a: Array<T>, -t: AP.Tree<T>, e: {AP.build(T, t) == a : Array<T>}, h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}) -> {A.Arrays.is_perfect(T, d, AP.build(T, t)) == True{} : Bool}:
1299	  %Equal.sym(Array<T>, AP.build(T, t), a, e) : {A.Arrays.is_perfect(T, d, _) == True{} : Bool}
1300	  h
1301	
1302	def AP.index_lt(+d: Nat, +i: U32) -> {Nat.is_lt(A.Arrays.index(d, i), A.Arrays.slots(d)) == True{} : Bool}:
1303	  %Equal.sym(U32, U32.sub(U32.shln(1, d), 1), U32{AP.lm(32n, d)}, AP.mask_lm(d)) : {Nat.is_lt(U32.to_nat(U32.and(i, _)), A.Arrays.slots(d)) == True{} : Bool}
1304	  AP.u32_mask_lt(i, d)
1305	
1306	# The tree forms of the model laws
1307	
1308	def AP.tree_perf(-T: Data, +d: Nat, +t: AP.Tree<T>, +i: U32, +v: T, h: {A.Arrays.is_perfect(T, d, AP.build(T, t)) == True{} : Bool}) -> {A.Arrays.is_perfect(T, d, AP.build(T, AP.set_top(T, t, i, v))) == True{} : Bool}:
1309	  +n = AP.size(T, t)
1310	  +j = AP.mask(n, i)
1311	  Equal.trans(Bool, A.Arrays.is_perfect(T, d, AP.build(T, AP.swap_t(T, t, n, j, v, AP.z(n, j)))), A.Arrays.is_perfect(T, d, AP.build(T, t)), True{}, AP.perf_swap(T, t, n, j, v, AP.z(n, j), d), h)
1312	
1313	def AP.tree_get(-T: Data, +d: Nat, +t: AP.Tree<T>, +hp: {A.Arrays.is_perfect(T, d, AP.build(T, t)) == True{} : Bool}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +i: U32) -> {List.get(&2, T, A.Arrays.leaves(T, AP.build(T, t)), A.Arrays.index(d, i)) == Some{AP.get_top(T, t, i)} : Maybe<&2, T>}:
1314	  +sh = U32.shln(1, d)
1315	  +j = AP.mask(sh, i)
1316	  %Equal.sym(U32, AP.size(T, t), sh, AP.size_perf(T, d, t, hp)) : {List.get(&2, T, A.Arrays.leaves(T, AP.build(T, t)), A.Arrays.index(d, i)) == Some{AP.get_v(T, t, _, AP.mask(_, i), AP.z(_, AP.mask(_, i)))} : Maybe<&2, T>}
1317	  AP.get_leaves(T, d, t, j, AP.z(sh, j), {==}, hd, hp, AP.index_lt(d, i))
1318	
1319	def AP.tree_set(-T: Data, +d: Nat, +t: AP.Tree<T>, +hp: {A.Arrays.is_perfect(T, d, AP.build(T, t)) == True{} : Bool}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +i: U32, +v: T) -> {A.Arrays.leaves(T, AP.build(T, AP.set_top(T, t, i, v))) == List.set(&2, T, A.Arrays.leaves(T, AP.build(T, t)), A.Arrays.index(d, i), v) : List<&2, T>}:
1320	  +sh = U32.shln(1, d)
1321	  +j = AP.mask(sh, i)
1322	  %Equal.sym(U32, AP.size(T, t), sh, AP.size_perf(T, d, t, hp)) : {A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, t, _, AP.mask(_, i), v, AP.z(_, AP.mask(_, i))))) == List.set(&2, T, A.Arrays.leaves(T, AP.build(T, t)), A.Arrays.index(d, i), v) : List<&2, T>}
1323	  AP.set_leaves(T, d, t, j, v, AP.z(sh, j), {==}, hd, hp, AP.index_lt(d, i))
1324	
1325	# The laws, each through the reflection of its array
1326	
1327	def AP.set_keeps_size.go(-T: Data, -a: Array<T>, +i: U32, +v: T, r: &t: AP.Tree<T> -> {AP.build(T, t) == a : Array<T>}) -> {Pair.snd(Array<T>, U32, Array.size(T, Array.set(T, a, i, v))) == Pair.snd(Array<T>, U32, Array.size(T, a)) : U32}:
1328	  (+t, e) = r
1329	  +n = AP.size(T, t)
1330	  +j = AP.mask(n, i)
1331	  +t2 = AP.set_top(T, t, i, v)
1332	  %e : {Pair.snd(Array<T>, U32, Array.size(T, Array.set(T, _, i, v))) == Pair.snd(Array<T>, U32, Array.size(T, _)) : U32}
1333	  %Equal.sym(Array<T>, Array.set(T, AP.build(T, t), i, v), AP.build(T, t2), AP.set_top_eq(T, t, i, v)) : {Pair.snd(Array<T>, U32, Array.size(T, _)) == Pair.snd(Array<T>, U32, Array.size(T, AP.build(T, t))) : U32}
1334	  %Equal.sym(Array<T> & U32, Array.size(T, AP.build(T, t2)), (AP.build(T, t2), AP.size(T, t2)), AP.size_eq(T, t2)) : {Pair.snd(Array<T>, U32, _) == Pair.snd(Array<T>, U32, Array.size(T, AP.build(T, t))) : U32}
1335	  %Equal.sym(Array<T> & U32, Array.size(T, AP.build(T, t)), (AP.build(T, t), n), AP.size_eq(T, t)) : {AP.size(T, t2) == Pair.snd(Array<T>, U32, _) : U32}
1336	  AP.swap_size(T, t, n, j, v, AP.z(n, j))
1337	
1338	def AP.get_new.go(-T: Data, +d: Nat, +v: T, +i: U32) -> {Pair.snd(Array<T>, T, Array.get(T, Array.new(T, d, v), i)) == v : T}:
1339	  +t = AP.tnew(T, d, v)
1340	  +n = AP.size(T, t)
1341	  +j = AP.mask(n, i)
1342	  %Equal.sym(Array<T>, Array.new(T, d, v), AP.build(T, t), AP.new_eq(T, d, v)) : {Pair.snd(Array<T>, T, Array.get(T, _, i)) == v : T}
1343	  %Equal.sym(Array<T> & T, Array.get(T, AP.build(T, t), i), (AP.build(T, t), AP.get_top(T, t, i)), AP.get_top_eq(T, t, i)) : {Pair.snd(Array<T>, T, _) == v : T}
1344	  AP.get_v_new(T, d, v, n, j, AP.z(n, j))
1345	
1346	def AP.set_perfect.go.body(-T: Data, +d: Nat, -a: Array<T>, h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}, +i: U32, +v: T, +t: AP.Tree<T>, +e: {AP.build(T, t) == a : Array<T>}) -> {A.Arrays.is_perfect(T, d, Array.set(T, a, i, v)) == True{} : Bool}:
1347	  %e : {A.Arrays.is_perfect(T, d, Array.set(T, _, i, v)) == True{} : Bool}
1348	  %Equal.sym(Array<T>, Array.set(T, AP.build(T, t), i, v), AP.build(T, AP.set_top(T, t, i, v)), AP.set_top_eq(T, t, i, v)) : {A.Arrays.is_perfect(T, d, _) == True{} : Bool}
1349	  AP.tree_perf(T, d, t, i, v, AP.perf_rw(T, d, a, t, e, h))
1350	
1351	def AP.set_perfect.go(-T: Data, +d: Nat, -a: Array<T>, h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}, +i: U32, +v: T, r: &t: AP.Tree<T> -> {AP.build(T, t) == a : Array<T>}) -> {A.Arrays.is_perfect(T, d, Array.set(T, a, i, v)) == True{} : Bool}:
1352	  (t, e) = r
1353	  AP.set_perfect.go.body(T, d, a, h, i, v, t, e)
1354	
1355	def AP.size_perfect.go.body(-T: Data, +d: Nat, -a: Array<T>, h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}, +t: AP.Tree<T>, +e: {AP.build(T, t) == a : Array<T>}) -> {Array.size(T, a) == (a, U32.shln(1, d)) : Array<T> & U32}:
1356	  %e : {Array.size(T, _) == (_, U32.shln(1, d)) : Array<T> & U32}
1357	  %Equal.sym(Array<T> & U32, Array.size(T, AP.build(T, t)), (AP.build(T, t), AP.size(T, t)), AP.size_eq(T, t)) : {_ == (AP.build(T, t), U32.shln(1, d)) : Array<T> & U32}
1358	  %Equal.sym(U32, AP.size(T, t), U32.shln(1, d), AP.size_perf(T, d, t, AP.perf_rw(T, d, a, t, e, h))) : {(AP.build(T, t), _) == (AP.build(T, t), U32.shln(1, d)) : Array<T> & U32}
1359	  {==}
1360	
1361	def AP.size_perfect.go(-T: Data, +d: Nat, -a: Array<T>, h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}, r: &t: AP.Tree<T> -> {AP.build(T, t) == a : Array<T>}) -> {Array.size(T, a) == (a, U32.shln(1, d)) : Array<T> & U32}:
1362	  (t, e) = r
1363	  AP.size_perfect.go.body(T, d, a, h, t, e)
1364	
1365	def AP.new_leaves.go(-T: Data, +d: Nat, +v: T) -> {A.Arrays.leaves(T, Array.new(T, d, v)) == List.replicate(T, A.Arrays.slots(d), v) : List<&2, T>}:
1366	  match d:
1367	    case 0n:
1368	      {==}
1369	    case 1n+ +p:
1370	      +s = A.Arrays.slots(p)
1371	      %Equal.sym(List<&2, T>, A.Arrays.leaves(T, Array.new(T, p, v)), List.replicate(T, s, v), AP.new_leaves.go(T, p, v)) : {List.append(&2, T, _, _) == List.replicate(T, Nat.double(s), v) : List<&2, T>}
1372	      %Equal.sym(Nat, Nat.double(s), Nat.add(s, s), AP.double_self(s)) : {List.append(&2, T, List.replicate(T, s, v), List.replicate(T, s, v)) == List.replicate(T, _, v) : List<&2, T>}
1373	      Equal.sym(List<&2, T>, List.replicate(T, Nat.add(s, s), v), List.append(&2, T, List.replicate(T, s, v), List.replicate(T, s, v)), AP.rep_add(T, s, s, v))
1374	
1375	def AP.model_length.go.body(-T: Data, +d: Nat, -a: Array<T>, h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}, +t: AP.Tree<T>, +e: {AP.build(T, t) == a : Array<T>}) -> {List.length(&2, T, A.Arrays.leaves(T, a)) == A.Arrays.slots(d) : Nat}:
1376	  %e : {List.length(&2, T, A.Arrays.leaves(T, _)) == A.Arrays.slots(d) : Nat}
1377	  AP.len_perf(T, d, t, AP.perf_rw(T, d, a, t, e, h))
1378	
1379	def AP.model_length.go(-T: Data, +d: Nat, -a: Array<T>, h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}, r: &t: AP.Tree<T> -> {AP.build(T, t) == a : Array<T>}) -> {List.length(&2, T, A.Arrays.leaves(T, a)) == A.Arrays.slots(d) : Nat}:
1380	  (t, e) = r
1381	  AP.model_length.go.body(T, d, a, h, t, e)
1382	
1383	def AP.model_get.go.body(-T: Data, +d: Nat, -a: Array<T>, h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +i: U32, +t: AP.Tree<T>, +e: {AP.build(T, t) == a : Array<T>}) -> {List.get(&2, T, A.Arrays.leaves(T, a), A.Arrays.index(d, i)) == Some{Pair.snd(Array<T>, T, Array.get(T, a, i))} : Maybe<&2, T>}:
1384	  %e : {List.get(&2, T, A.Arrays.leaves(T, _), A.Arrays.index(d, i)) == Some{Pair.snd(Array<T>, T, Array.get(T, _, i))} : Maybe<&2, T>}
1385	  %Equal.sym(Array<T> & T, Array.get(T, AP.build(T, t), i), (AP.build(T, t), AP.get_top(T, t, i)), AP.get_top_eq(T, t, i)) : {List.get(&2, T, A.Arrays.leaves(T, AP.build(T, t)), A.Arrays.index(d, i)) == Some{Pair.snd(Array<T>, T, _)} : Maybe<&2, T>}
1386	  AP.tree_get(T, d, t, AP.perf_rw(T, d, a, t, e, h), hd, i)
1387	
1388	def AP.model_get.go(-T: Data, +d: Nat, -a: Array<T>, h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +i: U32, r: &t: AP.Tree<T> -> {AP.build(T, t) == a : Array<T>}) -> {List.get(&2, T, A.Arrays.leaves(T, a), A.Arrays.index(d, i)) == Some{Pair.snd(Array<T>, T, Array.get(T, a, i))} : Maybe<&2, T>}:
1389	  (t, e) = r
1390	  AP.model_get.go.body(T, d, a, h, hd, i, t, e)
1391	
1392	def AP.model_set.go.body(-T: Data, +d: Nat, -a: Array<T>, h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +i: U32, +v: T, +t: AP.Tree<T>, +e: {AP.build(T, t) == a : Array<T>}) -> {A.Arrays.leaves(T, Array.set(T, a, i, v)) == List.set(&2, T, A.Arrays.leaves(T, a), A.Arrays.index(d, i), v) : List<&2, T>}:
1393	  %e : {A.Arrays.leaves(T, Array.set(T, _, i, v)) == List.set(&2, T, A.Arrays.leaves(T, _), A.Arrays.index(d, i), v) : List<&2, T>}
1394	  %Equal.sym(Array<T>, Array.set(T, AP.build(T, t), i, v), AP.build(T, AP.set_top(T, t, i, v)), AP.set_top_eq(T, t, i, v)) : {A.Arrays.leaves(T, _) == List.set(&2, T, A.Arrays.leaves(T, AP.build(T, t)), A.Arrays.index(d, i), v) : List<&2, T>}
1395	  AP.tree_set(T, d, t, AP.perf_rw(T, d, a, t, e, h), hd, i, v)
1396	
1397	def AP.model_set.go(-T: Data, +d: Nat, -a: Array<T>, h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +i: U32, +v: T, r: &t: AP.Tree<T> -> {AP.build(T, t) == a : Array<T>}) -> {A.Arrays.leaves(T, Array.set(T, a, i, v)) == List.set(&2, T, A.Arrays.leaves(T, a), A.Arrays.index(d, i), v) : List<&2, T>}:
1398	  (t, e) = r
1399	  AP.model_set.go.body(T, d, a, h, hd, i, v, t, e)
1400	
1401	def AP.get_set_other.go.body(-T: Data, +d: Nat, -a: Array<T>, h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +i: U32, +j: U32, +v: T, hij: {U32.is_eq(U32.and(i, U32.sub(U32.shln(1, d), 1)), U32.and(j, U32.sub(U32.shln(1, d), 1))) == False{} : Bool}, +t: AP.Tree<T>, +e: {AP.build(T, t) == a : Array<T>}) -> {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, a, i, v), j)) == Pair.snd(Array<T>, T, Array.get(T, a, j)) : T}:
1402	  +hp = AP.perf_rw(T, d, a, t, e, h)
1403	  +t2 = AP.set_top(T, t, i, v)
1404	  +l = A.Arrays.leaves(T, AP.build(T, t))
1405	  +ki = A.Arrays.index(d, i)
1406	  +kj = A.Arrays.index(d, j)
1407	  +m = U32.sub(U32.shln(1, d), 1)
1408	  +hk = Equal.trans(Bool, Nat.is_eq(ki, kj), U32.is_eq(U32.and(i, m), U32.and(j, m)), False{}, Equal.sym(Bool, U32.is_eq(U32.and(i, m), U32.and(j, m)), Nat.is_eq(ki, kj), AP.u32_eq(U32.and(i, m), U32.and(j, m))), hij)
1409	  %e : {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, _, i, v), j)) == Pair.snd(Array<T>, T, Array.get(T, _, j)) : T}
1410	  %Equal.sym(Array<T>, Array.set(T, AP.build(T, t), i, v), AP.build(T, t2), AP.set_top_eq(T, t, i, v)) : {Pair.snd(Array<T>, T, Array.get(T, _, j)) == Pair.snd(Array<T>, T, Array.get(T, AP.build(T, t), j)) : T}
1411	  %Equal.sym(Array<T> & T, Array.get(T, AP.build(T, t2), j), (AP.build(T, t2), AP.get_top(T, t2, j)), AP.get_top_eq(T, t2, j)) : {Pair.snd(Array<T>, T, _) == Pair.snd(Array<T>, T, Array.get(T, AP.build(T, t), j)) : T}
1412	  %Equal.sym(Array<T> & T, Array.get(T, AP.build(T, t), j), (AP.build(T, t), AP.get_top(T, t, j)), AP.get_top_eq(T, t, j)) : {AP.get_top(T, t2, j) == Pair.snd(Array<T>, T, _) : T}
1413	  +e1 = Equal.sym(Maybe<&2, T>, List.get(&2, T, A.Arrays.leaves(T, AP.build(T, t2)), kj), Some{AP.get_top(T, t2, j)}, AP.tree_get(T, d, t2, AP.tree_perf(T, d, t, i, v, hp), hd, j))
1414	  +e2 = Equal.cong(List<&2, T>, Maybe<&2, T>, xs => List.get(&2, T, xs, kj), A.Arrays.leaves(T, AP.build(T, t2)), List.set(&2, T, l, ki, v), AP.tree_set(T, d, t, hp, hd, i, v))
1415	  +e3 = AP.get_set_other(T, l, ki, kj, v, hk)
1416	  +e4 = AP.tree_get(T, d, t, hp, hd, j)
1417	  AP.some_inj(T, AP.get_top(T, t2, j), AP.get_top(T, t, j), Equal.trans(Maybe<&2, T>, Some{AP.get_top(T, t2, j)}, List.get(&2, T, l, kj), Some{AP.get_top(T, t, j)}, Equal.trans(Maybe<&2, T>, Some{AP.get_top(T, t2, j)}, List.get(&2, T, List.set(&2, T, l, ki, v), kj), List.get(&2, T, l, kj), Equal.trans(Maybe<&2, T>, Some{AP.get_top(T, t2, j)}, List.get(&2, T, A.Arrays.leaves(T, AP.build(T, t2)), kj), List.get(&2, T, List.set(&2, T, l, ki, v), kj), e1, e2), e3), e4))
1418	
1419	def AP.get_set_other.go(-T: Data, +d: Nat, -a: Array<T>, h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +i: U32, +j: U32, +v: T, hij: {U32.is_eq(U32.and(i, U32.sub(U32.shln(1, d), 1)), U32.and(j, U32.sub(U32.shln(1, d), 1))) == False{} : Bool}, r: &t: AP.Tree<T> -> {AP.build(T, t) == a : Array<T>}) -> {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, a, i, v), j)) == Pair.snd(Array<T>, T, Array.get(T, a, j)) : T}:
1420	  (t, e) = r
1421	  AP.get_set_other.go.body(T, d, a, h, hd, i, j, v, hij, t, e)
1422	
1423	def AP.index_of_nat.go(+d: Nat, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +k: Nat, +hk: {Nat.is_lt(k, A.Arrays.slots(d)) == True{} : Bool}) -> {A.Arrays.index(d, U32.from_nat(k)) == k : Nat}:
1424	  +a = U32.from_nat(k)
1425	  +fk = AP.from_nat(k, d, hk, AP.lt_le(d, 32n, hd))
1426	  %Equal.sym(U32, U32.sub(U32.shln(1, d), 1), U32{AP.lm(32n, d)}, AP.mask_lm(d)) : {U32.to_nat(U32.and(a, _)) == k : Nat}
1427	  %Equal.sym(U32, U32.and(a, U32{AP.lm(32n, d)}), a, AP.u32_and_id(a, d, AP.lt_rw_l(U32.to_nat(a), k, A.Arrays.slots(d), fk, hk))) : {U32.to_nat(_) == k : Nat}
1428	  fk
1429	
1430	
1431	# Arrays built from a Data list
1432	
1433	def AP.pred(n: Nat) -> Nat:
1434	  match n:
1435	    case 0n:
1436	      0n
1437	    case 1n+p:
1438	      p
1439	
1440	def AP.pred_cong(-a: Nat, -b: Nat, e: {1n+a == 1n+b : Nat}) -> {a == b : Nat}:
1441	  Equal.cong(Nat, Nat, n => AP.pred(n), 1n+a, 1n+b, e)
1442	
1443	def AP.tof(-T: Data, +d: Nat, +xs: List<&2, T>, +f: T) -> AP.Tree<T>:
1444	  match d:
1445	    case 0n:
1446	      APLeaf{A.Arrays.nth(T, xs, 0n, f)}
1447	    case 1n+p:
1448	      +s = A.Arrays.slots(p)
1449	      APNode{AP.tof(T, p, List.take(&2, T, xs, s), f), AP.tof(T, p, List.drop(&2, T, xs, s), f)}
1450	
1451	def AP.of_list_eq(-T: Data, +d: Nat, +xs: List<&2, T>, +f: T) -> {A.Arrays.of_list(T, d, xs, f) == AP.build(T, AP.tof(T, d, xs, f)) : Array<T>}:
1452	  match d:
1453	    case 0n:
1454	      {==}
1455	    case 1n+ +p:
1456	      +s = A.Arrays.slots(p)
1457	      +l = List.take(&2, T, xs, s)
1458	      +r = List.drop(&2, T, xs, s)
1459	      %Equal.sym(Array<T>, A.Arrays.of_list(T, p, l, f), AP.build(T, AP.tof(T, p, l, f)), AP.of_list_eq(T, p, l, f)) : {ANode{_, A.Arrays.of_list(T, p, r, f)} == ANode{AP.build(T, AP.tof(T, p, l, f)), AP.build(T, AP.tof(T, p, r, f))} : Array<T>}
1460	      %Equal.sym(Array<T>, A.Arrays.of_list(T, p, r, f), AP.build(T, AP.tof(T, p, r, f)), AP.of_list_eq(T, p, r, f)) : {ANode{AP.build(T, AP.tof(T, p, l, f)), _} == ANode{AP.build(T, AP.tof(T, p, l, f)), AP.build(T, AP.tof(T, p, r, f))} : Array<T>}
1461	      {==}
1462	
1463	def AP.tof_perf(-T: Data, +d: Nat, +xs: List<&2, T>, +f: T) -> {A.Arrays.is_perfect(T, d, AP.build(T, AP.tof(T, d, xs, f))) == True{} : Bool}:
1464	  match d:
1465	    case 0n:
1466	      {==}
1467	    case 1n+ +p:
1468	      +s = A.Arrays.slots(p)
1469	      +l = List.take(&2, T, xs, s)
1470	      +r = List.drop(&2, T, xs, s)
1471	      %Equal.sym(Bool, A.Arrays.is_perfect(T, p, AP.build(T, AP.tof(T, p, l, f))), True{}, AP.tof_perf(T, p, l, f)) : {Bool.and(_, A.Arrays.is_perfect(T, p, AP.build(T, AP.tof(T, p, r, f)))) == True{} : Bool}
1472	      AP.tof_perf(T, p, r, f)
1473	
1474	def AP.take_drop(-T: Data, xs: List<&2, T>, n: Nat) -> {List.append(&2, T, List.take(&2, T, xs, n), List.drop(&2, T, xs, n)) == xs : List<&2, T>}:
1475	  match xs n:
1476	    case Nil{} _:
1477	      {==}
1478	    case Con{x, t} 0n:
1479	      {==}
1480	    case Con{x, t} 1n+p:
1481	      AP.con_cong(T, x, List.append(&2, T, List.take(&2, T, t, p), List.drop(&2, T, t, p)), t, AP.take_drop(T, t, p))
1482	
1483	def AP.take_app(-T: Data, xs: List<&2, T>, ys: List<&2, T>) -> {List.take(&2, T, List.append(&2, T, xs, ys), List.length(&2, T, xs)) == xs : List<&2, T>}:
1484	  match xs:
1485	    case Nil{}:
1486	      match ys:
1487	        case Nil{}:
1488	          {==}
1489	        case Con{y, t}:
1490	          {==}
1491	    case Con{x, t}:
1492	      AP.con_cong(T, x, List.take(&2, T, List.append(&2, T, t, ys), List.length(&2, T, t)), t, AP.take_app(T, t, ys))
1493	
1494	def AP.drop_app(-T: Data, xs: List<&2, T>, ys: List<&2, T>) -> {List.drop(&2, T, List.append(&2, T, xs, ys), List.length(&2, T, xs)) == ys : List<&2, T>}:
1495	  match xs:
1496	    case Nil{}:
1497	      match ys:
1498	        case Nil{}:
1499	          {==}
1500	        case Con{y, t}:
1501	          {==}
1502	    case Con{x, t}:
1503	      AP.drop_app(T, t, ys)
1504	
1505	# a list of n + m elements cut after n: n, then m elements
1506	def AP.len_take(-T: Data, xs: List<&2, T>, n: Nat, -m: Nat, h: {List.length(&2, T, xs) == Nat.add(n, m) : Nat}) -> {List.length(&2, T, List.take(&2, T, xs, n)) == n : Nat}:
1507	  match xs n:
1508	    case Nil{} 0n:
1509	      {==}
1510	    case Nil{} 1n+p:
1511	      Empty.absurd({List.length(&2, T, List.take(&2, T, Nil{}, 1n+p)) == 1n+p : Nat}, AP.sz(Nat.add(p, m), Equal.sym(Nat, 0n, 1n+Nat.add(p, m), h)))
1512	    case Con{x, t} 0n:
1513	      {==}
1514	    case Con{x, t} 1n+p:
1515	      AP.succ_cong(List.length(&2, T, List.take(&2, T, t, p)), p, AP.len_take(T, t, p, m, AP.pred_cong(List.length(&2, T, t), Nat.add(p, m), h)))
1516	
1517	def AP.len_drop(-T: Data, xs: List<&2, T>, n: Nat, -m: Nat, h: {List.length(&2, T, xs) == Nat.add(n, m) : Nat}) -> {List.length(&2, T, List.drop(&2, T, xs, n)) == m : Nat}:
1518	  match xs n:
1519	    case Nil{} 0n:
1520	      h
1521	    case Nil{} 1n+p:
1522	      Empty.absurd({List.length(&2, T, List.drop(&2, T, Nil{}, 1n+p)) == m : Nat}, AP.sz(Nat.add(p, m), Equal.sym(Nat, 0n, 1n+Nat.add(p, m), h)))
1523	    case Con{x, t} 0n:
1524	      h
1525	    case Con{x, t} 1n+p:
1526	      AP.len_drop(T, t, p, m, AP.pred_cong(List.length(&2, T, t), Nat.add(p, m), h))
1527	
1528	def AP.one_elem(-T: Data, xs: List<&2, T>, -f: T, h: {List.length(&2, T, xs) == 1n : Nat}) -> {Con{A.Arrays.nth(T, xs, 0n, f), Nil{}} == xs : List<&2, T>}:
1529	  match xs:
1530	    case Nil{}:
1531	      Empty.absurd({Con{A.Arrays.nth(T, Nil{}, 0n, f), Nil{}} == Nil{} : List<&2, T>}, AP.sz(0n, Equal.sym(Nat, 0n, 1n, h)))
1532	    case Con{x, t}:
1533	      match t:
1534	        case Nil{}:
1535	          {==}
1536	        case Con{y, u}:
1537	          Empty.absurd({Con{A.Arrays.nth(T, Con{x, Con{y, u}}, 0n, f), Nil{}} == Con{x, Con{y, u}} : List<&2, T>}, AP.sz(List.length(&2, T, u), AP.pred_cong(1n+List.length(&2, T, u), 0n, h)))
1538	
1539	def AP.tof_leaves(-T: Data, +d: Nat, +xs: List<&2, T>, +f: T, +h: {List.length(&2, T, xs) == A.Arrays.slots(d) : Nat}) -> {A.Arrays.leaves(T, AP.build(T, AP.tof(T, d, xs, f))) == xs : List<&2, T>}:
1540	  match d:
1541	    case 0n:
1542	      AP.one_elem(T, xs, f, h)
1543	    case 1n+ +p:
1544	      +s = A.Arrays.slots(p)
1545	      +l = List.take(&2, T, xs, s)
1546	      +r = List.drop(&2, T, xs, s)
1547	      +h2 = Equal.trans(Nat, List.length(&2, T, xs), Nat.double(s), Nat.add(s, s), h, AP.double_self(s))
1548	      %Equal.sym(List<&2, T>, A.Arrays.leaves(T, AP.build(T, AP.tof(T, p, l, f))), l, AP.tof_leaves(T, p, l, f, AP.len_take(T, xs, s, s, h2))) : {List.append(&2, T, _, A.Arrays.leaves(T, AP.build(T, AP.tof(T, p, r, f)))) == xs : List<&2, T>}
1549	      %Equal.sym(List<&2, T>, A.Arrays.leaves(T, AP.build(T, AP.tof(T, p, r, f))), r, AP.tof_leaves(T, p, r, f, AP.len_drop(T, xs, s, s, h2))) : {List.append(&2, T, l, _) == xs : List<&2, T>}
1550	      AP.take_drop(T, xs, s)
1551	
1552	# a perfect tree is the tree of its own leaves
1553	def AP.tree_ext(-T: Data, +d: Nat, +t: AP.Tree<T>, +f: T, +hp: {A.Arrays.is_perfect(T, d, AP.build(T, t)) == True{} : Bool}) -> {AP.build(T, t) == AP.build(T, AP.tof(T, d, A.Arrays.leaves(T, AP.build(T, t)), f)) : Array<T>}:
1554	  match d t:
1555	    case 0n APLeaf{x}:
1556	      {==}
1557	    case 0n APNode{xs, ys}:
1558	      Empty.absurd({AP.build(T, APNode{xs, ys}) == AP.build(T, AP.tof(T, 0n, A.Arrays.leaves(T, AP.build(T, APNode{xs, ys})), f)) : Array<T>}, AP.ft(hp))
1559	    case 1n+p APLeaf{x}:
1560	      Empty.absurd({AP.build(T, APLeaf{x}) == AP.build(T, AP.tof(T, 1n+p, A.Arrays.leaves(T, AP.build(T, APLeaf{x})), f)) : Array<T>}, AP.ft(hp))
1561	    case 1n+ +p APNode{xs, ys}:
1562	      +s = A.Arrays.slots(p)
1563	      +lx = A.Arrays.leaves(T, AP.build(T, xs))
1564	      +ly = A.Arrays.leaves(T, AP.build(T, ys))
1565	      +hpx = AP.and_l(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp)
1566	      +hpy = AP.and_r(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp)
1567	      +hl = AP.len_perf(T, p, xs, hpx)
1568	      %hl : {ANode{AP.build(T, xs), AP.build(T, ys)} == ANode{AP.build(T, AP.tof(T, p, List.take(&2, T, List.append(&2, T, lx, ly), _), f)), AP.build(T, AP.tof(T, p, List.drop(&2, T, List.append(&2, T, lx, ly), _), f))} : Array<T>}
1569	      %Equal.sym(List<&2, T>, List.take(&2, T, List.append(&2, T, lx, ly), List.length(&2, T, lx)), lx, AP.take_app(T, lx, ly)) : {ANode{AP.build(T, xs), AP.build(T, ys)} == ANode{AP.build(T, AP.tof(T, p, _, f)), AP.build(T, AP.tof(T, p, List.drop(&2, T, List.append(&2, T, lx, ly), List.length(&2, T, lx)), f))} : Array<T>}
1570	      %Equal.sym(List<&2, T>, List.drop(&2, T, List.append(&2, T, lx, ly), List.length(&2, T, lx)), ly, AP.drop_app(T, lx, ly)) : {ANode{AP.build(T, xs), AP.build(T, ys)} == ANode{AP.build(T, AP.tof(T, p, lx, f)), AP.build(T, AP.tof(T, p, _, f))} : Array<T>}
1571	      %AP.tree_ext(T, p, xs, f, hpx) : {ANode{AP.build(T, xs), AP.build(T, ys)} == ANode{_, AP.build(T, AP.tof(T, p, ly, f))} : Array<T>}
1572	      %AP.tree_ext(T, p, ys, f, hpy) : {ANode{AP.build(T, xs), AP.build(T, ys)} == ANode{AP.build(T, xs), _} : Array<T>}
1573	      {==}
1574	
1575	def AP.nth_get(-T: Data, -xs: List<&2, T>, -k: Nat, -f: T, -g: T, e: {List.get(&2, T, xs, k) == Some{g} : Maybe<&2, T>}) -> {A.Arrays.nth(T, xs, k, f) == g : T}:
1576	  %Equal.sym(Maybe<&2, T>, List.get(&2, T, xs, k), Some{g}, e) : {A.Arrays.nth.or(T, _, f) == g : T}
1577	  {==}
1578	
1579	def AP.set_length(-T: Data, xs: List<&2, T>, k: Nat, -v: T) -> {List.length(&2, T, List.set(&2, T, xs, k, v)) == List.length(&2, T, xs) : Nat}:
1580	  match xs k:
1581	    case Nil{} _:
1582	      {==}
1583	    case Con{x, t} 0n:
1584	      {==}
1585	    case Con{x, t} 1n+p:
1586	      AP.succ_cong(List.length(&2, T, List.set(&2, T, t, p, v)), List.length(&2, T, t), AP.set_length(T, t, p, v))
1587	
1588	def AP.get_set_same(-T: Data, xs: List<&2, T>, k: Nat, -v: T, h: {Nat.is_lt(k, List.length(&2, T, xs)) == True{} : Bool}) -> {List.get(&2, T, List.set(&2, T, xs, k, v), k) == Some{v} : Maybe<&2, T>}:
1589	  match xs k:
1590	    case Nil{} _:
1591	      Empty.absurd({List.get(&2, T, List.set(&2, T, Nil{}, k, v), k) == Some{v} : Maybe<&2, T>}, AP.ft(Equal.trans(Bool, False{}, Nat.is_lt(k, 0n), True{}, Equal.sym(Bool, Nat.is_lt(k, 0n), False{}, AP.lt_zero(k)), h)))
1592	    case Con{x, t} 0n:
1593	      {==}
1594	    case Con{x, t} 1n+p:
1595	      AP.get_set_same(T, t, p, v, h)
1596	
1597	def AP.get_rep(-T: Data, n: Nat, k: Nat, +v: T, h: {Nat.is_lt(k, n) == True{} : Bool}) -> {List.get(&2, T, List.replicate(T, n, v), k) == Some{v} : Maybe<&2, T>}:
1598	  match n k:
1599	    case 0n _:
1600	      Empty.absurd({List.get(&2, T, List.replicate(T, 0n, v), k) == Some{v} : Maybe<&2, T>}, AP.ft(Equal.trans(Bool, False{}, Nat.is_lt(k, 0n), True{}, Equal.sym(Bool, Nat.is_lt(k, 0n), False{}, AP.lt_zero(k)), h)))
1601	    case 1n+p 0n:
1602	      {==}
1603	    case 1n+p 1n+q:
1604	      AP.get_rep(T, p, q, v, h)
1605	
1606	def AP.tnew_tof(-T: Data, +d: Nat, +v: T) -> {AP.build(T, AP.tnew(T, d, v)) == AP.build(T, AP.tof(T, d, List.replicate(T, A.Arrays.slots(d), v), v)) : Array<T>}:
1607	  +t = AP.tnew(T, d, v)
1608	  +hp = Equal.trans(Bool, A.Arrays.is_perfect(T, d, AP.build(T, t)), A.Arrays.is_perfect(T, d, Array.new(T, d, v)), True{}, Equal.cong(Array<T>, Bool, a => A.Arrays.is_perfect(T, d, a), AP.build(T, t), Array.new(T, d, v), Equal.sym(Array<T>, Array.new(T, d, v), AP.build(T, t), AP.new_eq(T, d, v))), AP.new_perf(T, d, v))
1609	  +hl = Equal.trans(List<&2, T>, A.Arrays.leaves(T, AP.build(T, t)), A.Arrays.leaves(T, Array.new(T, d, v)), List.replicate(T, A.Arrays.slots(d), v), Equal.cong(Array<T>, List<&2, T>, a => A.Arrays.leaves(T, a), AP.build(T, t), Array.new(T, d, v), Equal.sym(Array<T>, Array.new(T, d, v), AP.build(T, t), AP.new_eq(T, d, v))), AP.new_leaves.go(T, d, v))
1610	  %hl : {AP.build(T, t) == AP.build(T, AP.tof(T, d, _, v)) : Array<T>}
1611	  AP.tree_ext(T, d, t, v, hp)
1612	
1613	def AP.reflect_list(-T: Data, +d: Nat, -a: Array<T>, h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}, +f: T, +t: AP.Tree<T>, +e: {AP.build(T, t) == a : Array<T>}) -> &xs: List<&2, T> -> {A.Arrays.of_list(T, d, xs, f) == a : Array<T>} & {List.length(&2, T, xs) == A.Arrays.slots(d) : Nat}:
1614	  +hp = AP.perf_rw(T, d, a, t, e, h)
1615	  +xs = A.Arrays.leaves(T, AP.build(T, t))
1616	  +e1 = Equal.trans(Array<T>, A.Arrays.of_list(T, d, xs, f), AP.build(T, AP.tof(T, d, xs, f)), a, AP.of_list_eq(T, d, xs, f), Equal.trans(Array<T>, AP.build(T, AP.tof(T, d, xs, f)), AP.build(T, t), a, Equal.sym(Array<T>, AP.build(T, t), AP.build(T, AP.tof(T, d, xs, f)), AP.tree_ext(T, d, t, f, hp)), e))
1617	  (xs, (e1, AP.len_perf(T, d, t, hp)))
1618	
1619	def AP.ol_sym(-T: Data, +d: Nat, +xs: List<&2, T>, +f: T) -> {AP.build(T, AP.tof(T, d, xs, f)) == A.Arrays.of_list(T, d, xs, f) : Array<T>}:
1620	  Equal.sym(Array<T>, A.Arrays.of_list(T, d, xs, f), AP.build(T, AP.tof(T, d, xs, f)), AP.of_list_eq(T, d, xs, f))
1621	
1622	def AP.of_list_get.go(-T: Data, +d: Nat, +xs: List<&2, T>, +f: T, +hl: {List.length(&2, T, xs) == A.Arrays.slots(d) : Nat}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +i: U32) -> {Array.get(T, A.Arrays.of_list(T, d, xs, f), i) == (A.Arrays.of_list(T, d, xs, f), A.Arrays.nth(T, xs, A.Arrays.index(d, i), f)) : Array<T> & T}:
1623	  +t = AP.tof(T, d, xs, f)
1624	  +k = A.Arrays.index(d, i)
1625	  +g = AP.get_top(T, t, i)
1626	  +el = AP.tof_leaves(T, d, xs, f, hl)
1627	  +eg = Equal.trans(Maybe<&2, T>, List.get(&2, T, xs, k), List.get(&2, T, A.Arrays.leaves(T, AP.build(T, t)), k), Some{g}, Equal.cong(List<&2, T>, Maybe<&2, T>, ys => List.get(&2, T, ys, k), xs, A.Arrays.leaves(T, AP.build(T, t)), Equal.sym(List<&2, T>, A.Arrays.leaves(T, AP.build(T, t)), xs, el)), AP.tree_get(T, d, t, AP.tof_perf(T, d, xs, f), hd, i))
1628	  %AP.ol_sym(T, d, xs, f) : {Array.get(T, _, i) == (_, A.Arrays.nth(T, xs, k, f)) : Array<T> & T}
1629	  %Equal.sym(Array<T> & T, Array.get(T, AP.build(T, t), i), (AP.build(T, t), g), AP.get_top_eq(T, t, i)) : {_ == (AP.build(T, t), A.Arrays.nth(T, xs, k, f)) : Array<T> & T}
1630	  %AP.nth_get(T, xs, k, f, g, eg) : {(AP.build(T, t), _) == (AP.build(T, t), A.Arrays.nth(T, xs, k, f)) : Array<T> & T}
1631	  {==}
1632	
1633	def AP.of_list_set.go(-T: Data, +d: Nat, +xs: List<&2, T>, +f: T, +hl: {List.length(&2, T, xs) == A.Arrays.slots(d) : Nat}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +i: U32, +v: T) -> {Array.set(T, A.Arrays.of_list(T, d, xs, f), i, v) == A.Arrays.of_list(T, d, List.set(&2, T, xs, A.Arrays.index(d, i), v), f) : Array<T>}:
1634	  +t = AP.tof(T, d, xs, f)
1635	  +k = A.Arrays.index(d, i)
1636	  +t2 = AP.set_top(T, t, i, v)
1637	  +l2 = List.set(&2, T, xs, k, v)
1638	  +el = AP.tof_leaves(T, d, xs, f, hl)
1639	  +hp = AP.tof_perf(T, d, xs, f)
1640	  +el2 = Equal.trans(List<&2, T>, A.Arrays.leaves(T, AP.build(T, t2)), List.set(&2, T, A.Arrays.leaves(T, AP.build(T, t)), k, v), l2, AP.tree_set(T, d, t, hp, hd, i, v), Equal.cong(List<&2, T>, List<&2, T>, ys => List.set(&2, T, ys, k, v), A.Arrays.leaves(T, AP.build(T, t)), xs, el))
1641	  %AP.ol_sym(T, d, xs, f) : {Array.set(T, _, i, v) == A.Arrays.of_list(T, d, l2, f) : Array<T>}
1642	  %Equal.sym(Array<T>, Array.set(T, AP.build(T, t), i, v), AP.build(T, t2), AP.set_top_eq(T, t, i, v)) : {_ == A.Arrays.of_list(T, d, l2, f) : Array<T>}
1643	  %AP.ol_sym(T, d, l2, f) : {AP.build(T, t2) == _ : Array<T>}
1644	  %el2 : {AP.build(T, t2) == AP.build(T, AP.tof(T, d, _, f)) : Array<T>}
1645	  AP.tree_ext(T, d, t2, f, AP.tree_perf(T, d, t, i, v, hp))
1646	
1647	def AP.of_list_size.go(-T: Data, +d: Nat, +xs: List<&2, T>, +f: T) -> {Array.size(T, A.Arrays.of_list(T, d, xs, f)) == (A.Arrays.of_list(T, d, xs, f), U32.shln(1, d)) : Array<T> & U32}:
1648	  +t = AP.tof(T, d, xs, f)
1649	  %AP.ol_sym(T, d, xs, f) : {Array.size(T, _) == (_, U32.shln(1, d)) : Array<T> & U32}
1650	  %Equal.sym(Array<T> & U32, Array.size(T, AP.build(T, t)), (AP.build(T, t), AP.size(T, t)), AP.size_eq(T, t)) : {_ == (AP.build(T, t), U32.shln(1, d)) : Array<T> & U32}
1651	  %Equal.sym(U32, AP.size(T, t), U32.shln(1, d), AP.size_perf(T, d, t, AP.tof_perf(T, d, xs, f))) : {(AP.build(T, t), _) == (AP.build(T, t), U32.shln(1, d)) : Array<T> & U32}
1652	  {==}
1653	
1654	def AP.reflect.go(-T: Data, +d: Nat, -a: Array<T>, h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}, +f: T, r: &t: AP.Tree<T> -> {AP.build(T, t) == a : Array<T>}) -> &xs: List<&2, T> -> {A.Arrays.of_list(T, d, xs, f) == a : Array<T>} & {List.length(&2, T, xs) == A.Arrays.slots(d) : Nat}:
1655	  (t, e) = r
1656	  AP.reflect_list(T, d, a, h, f, t, e)
1657	
1658	# The laws
1659	
1660	def Laws.get_same_array(T, a, i):
1661	  AP.get_same_array.go(T, a, i, AP.reflect(T, a))
1662	
1663	def Laws.get_set_same(T, a, i, v):
1664	  AP.get_set_same.go(T, a, i, v, AP.reflect(T, a))
1665	
1666	def Laws.set_keeps_size(T, a, i, v):
1667	  AP.set_keeps_size.go(T, a, i, v, AP.reflect(T, a))
1668	
1669	def Laws.get_new(T, d, v, i):
1670	  AP.get_new.go(T, d, v, i)
1671	
1672	def Laws.new_perfect(T, d, v):
1673	  AP.new_perf(T, d, v)
1674	
1675	def Laws.set_perfect(T, d, a, h, i, v):
1676	  AP.set_perfect.go(T, d, a, h, i, v, AP.reflect(T, a))
1677	
1678	def Laws.size_perfect(T, d, a, h):
1679	  AP.size_perfect.go(T, d, a, h, AP.reflect(T, a))
1680	
1681	def Laws.new_leaves(T, d, v):
1682	  AP.new_leaves.go(T, d, v)
1683	
1684	def Laws.model_length(T, d, a, h):
1685	  AP.model_length.go(T, d, a, h, AP.reflect(T, a))
1686	
1687	def Laws.model_get(T, d, a, h, hd, i):
1688	  AP.model_get.go(T, d, a, h, hd, i, AP.reflect(T, a))
1689	
1690	def Laws.model_set(T, d, a, h, hd, i, v):
1691	  AP.model_set.go(T, d, a, h, hd, i, v, AP.reflect(T, a))
1692	
1693	def Laws.get_set_other(T, d, a, h, hd, i, j, v, hij):
1694	  AP.get_set_other.go(T, d, a, h, hd, i, j, v, hij, AP.reflect(T, a))
1695	
1696	def Laws.index_below(d, i):
1697	  AP.index_lt(d, i)
1698	
1699	def Laws.index_of_nat(d, hd, k, hk):
1700	  AP.index_of_nat.go(d, hd, k, hk)
1701	
1702	def Laws.witness_perfect():
1703	  {==}
1704	
1705	def Laws.witness_other():
1706	  {==}
1707	
1708	def Laws.witness_index():
1709	  {==}
1710	
1711	def Laws.vector_wrap():
1712	  {==}
1713	
1714	def Laws.vector_leaves():
1715	  {==}
1716	
1717	def Laws.vector_index():
1718	  {==}
1719	
1720	def Laws.vector_not_perfect():
1721	  {==}
1722	
1723	def Laws.of_list_perfect(T, d, xs, f):
1724	  %AP.ol_sym(T, d, xs, f) : {A.Arrays.is_perfect(T, d, _) == True{} : Bool}
1725	  AP.tof_perf(T, d, xs, f)
1726	
1727	def Laws.of_list_leaves(T, d, xs, f, hl):
1728	  %AP.ol_sym(T, d, xs, f) : {A.Arrays.leaves(T, _) == xs : List<&2, T>}
1729	  AP.tof_leaves(T, d, xs, f, hl)
1730	
1731	def Laws.of_list_size(T, d, xs, f):
1732	  AP.of_list_size.go(T, d, xs, f)
1733	
1734	def Laws.of_list_get(T, d, xs, f, hl, hd, i):
1735	  AP.of_list_get.go(T, d, xs, f, hl, hd, i)
1736	
1737	def Laws.of_list_set(T, d, xs, f, hl, hd, i, v):
1738	  AP.of_list_set.go(T, d, xs, f, hl, hd, i, v)
1739	
1740	def Laws.of_list_new(T, d, v):
1741	  Equal.trans(Array<T>, Array.new(T, d, v), AP.build(T, AP.tnew(T, d, v)), A.Arrays.of_list(T, d, List.replicate(T, A.Arrays.slots(d), v), v), AP.new_eq(T, d, v), Equal.trans(Array<T>, AP.build(T, AP.tnew(T, d, v)), AP.build(T, AP.tof(T, d, List.replicate(T, A.Arrays.slots(d), v), v)), A.Arrays.of_list(T, d, List.replicate(T, A.Arrays.slots(d), v), v), AP.tnew_tof(T, d, v), AP.ol_sym(T, d, List.replicate(T, A.Arrays.slots(d), v), v)))
1742	
1743	def Laws.reflect(T, d, a, h, f):
1744	  AP.reflect.go(T, d, a, h, f, AP.reflect(T, a))
1745	
1746	def Laws.set_length(T, xs, k, v):
1747	  AP.set_length(T, xs, k, v)
1748	
1749	def Laws.nth_set_same(T, xs, k, v, f, h):
1750	  AP.nth_get(T, List.set(&2, T, xs, k, v), k, f, v, AP.get_set_same(T, xs, k, v, h))
1751	
1752	def Laws.nth_set_other(T, xs, k, m, v, f, h):
1753	  Equal.cong(Maybe<&2, T>, T, x => A.Arrays.nth.or(T, x, f), List.get(&2, T, List.set(&2, T, xs, k, v), m), List.get(&2, T, xs, m), AP.get_set_other(T, xs, k, m, v, h))
1754	
1755	def Laws.nth_replicate(T, n, v, k, f, h):
1756	  AP.nth_get(T, List.replicate(T, n, v), k, f, v, AP.get_rep(T, n, k, v, h))
1757	
1758	def Laws.witness_list():
1759	  {==}
1760	
1761	def Laws.vector_of_list():
1762	  {==}
1763	
1764	# An index between 2^d and 2^(d+1) wraps to its distance from 2^d
1765	# (index_wrap)
1766	
1767	def AP.wh0(b: Bool, -s: Nat, -k: Nat, e: {AP.bv(b, 0n) == Nat.add(Nat.double(1n+s), k) : Nat}) -> Empty:
1768	  match b:
1769	    case False{}:
1770	      AP.sz(1n+Nat.add(Nat.double(s), k), Equal.sym(Nat, 0n, 2n+Nat.add(Nat.double(s), k), e))
1771	    case True{}:
1772	      AP.sz(Nat.add(Nat.double(s), k), Equal.sym(Nat, 0n, 1n+Nat.add(Nat.double(s), k), AP.pred_cong(0n, 1n+Nat.add(Nat.double(s), k), e)))
1773	
1774	# bv(b, x) = 2s + k: k is bv(b, x - s)
1775	def AP.wh(x: Nat, s: Nat, b: Bool, -k: Nat, e: {AP.bv(b, x) == Nat.add(Nat.double(s), k) : Nat}) -> {k == AP.bv(b, Nat.sub(x, s)) : Nat}:
1776	  match x s:
1777	    case 0n 0n:
1778	      Equal.sym(Nat, AP.bv(b, 0n), k, e)
1779	    case 0n 1n+q:
1780	      Empty.absurd({k == AP.bv(b, Nat.sub(0n, 1n+q)) : Nat}, AP.wh0(b, q, k, e))
1781	    case 1n+p 0n:
1782	      Equal.sym(Nat, AP.bv(b, 1n+p), k, e)
1783	    case 1n+p 1n+q:
1784	      match b:
1785	        case False{}:
1786	          AP.wh(p, q, False{}, k, AP.pred_cong(Nat.double(p), Nat.add(Nat.double(q), k), AP.pred_cong(1n+Nat.double(p), 1n+Nat.add(Nat.double(q), k), e)))
1787	        case True{}:
1788	          AP.wh(p, q, True{}, k, AP.pred_cong(1n+Nat.double(p), Nat.add(Nat.double(q), k), AP.pred_cong(2n+Nat.double(p), 1n+Nat.add(Nat.double(q), k), e)))
1789	
1790	# bv(b, x) = 2s + k: x is s + (x - s)
1791	def AP.wh2(x: Nat, s: Nat, b: Bool, -k: Nat, e: {AP.bv(b, x) == Nat.add(Nat.double(s), k) : Nat}) -> {x == Nat.add(s, Nat.sub(x, s)) : Nat}:
1792	  match x s:
1793	    case 0n 0n:
1794	      {==}
1795	    case 0n 1n+q:
1796	      Empty.absurd({0n == Nat.add(1n+q, Nat.sub(0n, 1n+q)) : Nat}, AP.wh0(b, q, k, e))
1797	    case 1n+p 0n:
1798	      {==}
1799	    case 1n+p 1n+q:
1800	      match b:
1801	        case False{}:
1802	          AP.succ_cong(p, Nat.add(q, Nat.sub(p, q)), AP.wh2(p, q, False{}, k, AP.pred_cong(Nat.double(p), Nat.add(Nat.double(q), k), AP.pred_cong(1n+Nat.double(p), 1n+Nat.add(Nat.double(q), k), e))))
1803	        case True{}:
1804	          AP.succ_cong(p, Nat.add(q, Nat.sub(p, q)), AP.wh2(p, q, True{}, k, AP.pred_cong(1n+Nat.double(p), Nat.add(Nat.double(q), k), AP.pred_cong(2n+Nat.double(p), 1n+Nat.add(Nat.double(q), k), e))))
1805	
1806	def AP.lt_rw_k(-k: Nat, -x: Nat, -s: Nat, e: {k == x : Nat}, h: {Nat.is_lt(k, s) == True{} : Bool}) -> {Nat.is_lt(x, s) == True{} : Bool}:
1807	  %e : {Nat.is_lt(_, s) == True{} : Bool}
1808	  h
1809	
1810	# a word of value 2^d + k, k < 2^d, masked to its low d bits, is k
1811	def AP.wrap(n: Nat, w: Word(n), +d: Nat, +k: Nat, +e: {Word.to_nat(n, w) == Nat.add(A.Arrays.slots(d), k) : Nat}, hk: {Nat.is_lt(k, A.Arrays.slots(d)) == True{} : Bool}, hd: {Nat.is_lt(d, n) == True{} : Bool}) -> {Word.to_nat(n, Word.and(n, w, AP.lm(n, d))) == k : Nat}:
1812	  match n:
1813	    case 0n:
1814	      Empty.absurd({Word.to_nat(0n, Word.and(0n, w, AP.lm(0n, d))) == k : Nat}, AP.tf(Equal.trans(Bool, True{}, Nat.is_lt(d, 0n), False{}, Equal.sym(Bool, Nat.is_lt(d, 0n), True{}, hd), AP.lt_zero(d))))
1815	    case 1n+ +q:
1816	      match w d:
1817	        case WCon{+b0, +t0} 0n:
1818	          +x = Word.to_nat(1n+q, Word.and(1n+q, WCon{b0, t0}, AP.lm(1n+q, 0n)))
1819	          Equal.trans(Nat, x, 0n, k, AP.lt_one(x, AP.mask_lt(1n+q, WCon{b0, t0}, 0n)), Equal.sym(Nat, k, 0n, AP.lt_one(k, hk)))
1820	        case WCon{False{}, +t} 1n+ +dd:
1821	          +s = A.Arrays.slots(dd)
1822	          +v = Nat.sub(Word.to_nat(q, t), s)
1823	          +ek = AP.wh(Word.to_nat(q, t), s, False{}, k, e)
1824	          +ev = AP.wh2(Word.to_nat(q, t), s, False{}, k, e)
1825	          +hv = AP.lt_bv_inv(False{}, v, s, AP.lt_rw_k(k, Nat.double(v), Nat.double(s), ek, hk))
1826	          +x = Word.to_nat(q, Word.and(q, t, AP.lm(q, dd)))
1827	          Equal.trans(Nat, Nat.double(x), Nat.double(v), k, AP.double_cong(x, v, AP.wrap(q, t, dd, v, ev, hv, hd)), Equal.sym(Nat, k, Nat.double(v), ek))
1828	        case WCon{True{}, +t} 1n+ +dd:
1829	          +s = A.Arrays.slots(dd)
1830	          +v = Nat.sub(Word.to_nat(q, t), s)
1831	          +ek = AP.wh(Word.to_nat(q, t), s, True{}, k, e)
1832	          +ev = AP.wh2(Word.to_nat(q, t), s, True{}, k, e)
1833	          +hv = AP.lt_bv_inv(True{}, v, s, AP.lt_rw_k(k, 1n+Nat.double(v), Nat.double(s), ek, hk))
1834	          +x = Word.to_nat(q, Word.and(q, t, AP.lm(q, dd)))
1835	          Equal.trans(Nat, 1n+Nat.double(x), 1n+Nat.double(v), k, AP.succ_cong(Nat.double(x), Nat.double(v), AP.double_cong(x, v, AP.wrap(q, t, dd, v, ev, hv, hd))), Equal.sym(Nat, k, 1n+Nat.double(v), ek))
1836	
1837	def AP.u32_wrap(a: U32, +d: Nat, +k: Nat, e: {U32.to_nat(a) == Nat.add(A.Arrays.slots(d), k) : Nat}, hk: {Nat.is_lt(k, A.Arrays.slots(d)) == True{} : Bool}, hd: {Nat.is_lt(d, 32n) == True{} : Bool}) -> {U32.to_nat(U32.and(a, U32{AP.lm(32n, d)})) == k : Nat}:
1838	  match a:
1839	    case U32{w}:
1840	      AP.wrap(32n, w, d, k, e, hk, hd)
1841	
1842	# s + k < 2s, for k < s
1843	def AP.wrap_lt(+s: Nat, +k: Nat, hk: {Nat.is_lt(k, s) == True{} : Bool}) -> {Nat.is_lt(Nat.add(s, k), Nat.double(s)) == True{} : Bool}:
1844	  %Equal.sym(Nat, Nat.double(s), Nat.add(s, s), AP.double_self(s)) : {Nat.is_lt(Nat.add(s, k), _) == True{} : Bool}
1845	  Equal.trans(Bool, Nat.is_lt(Nat.add(s, k), Nat.add(s, s)), Nat.is_lt(k, s), True{}, AP.lt_cancel(s, k, s), hk)
1846	
1847	def AP.index_wrap.go(+d: Nat, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +k: Nat, +hk: {Nat.is_lt(k, A.Arrays.slots(d)) == True{} : Bool}) -> {A.Arrays.index(d, U32.from_nat(Nat.add(A.Arrays.slots(d), k))) == k : Nat}:
1848	  +s = A.Arrays.slots(d)
1849	  +a = U32.from_nat(Nat.add(s, k))
1850	  +hd1 = Equal.trans(Bool, Nat.is_le(1n+d, 32n), Nat.is_lt(d, 32n), True{}, AP.le_succ(d, 32n), hd)
1851	  +fk = AP.from_nat(Nat.add(s, k), 1n+d, AP.wrap_lt(s, k, hk), hd1)
1852	  %Equal.sym(U32, U32.sub(U32.shln(1, d), 1), U32{AP.lm(32n, d)}, AP.mask_lm(d)) : {U32.to_nat(U32.and(a, _)) == k : Nat}
1853	  AP.u32_wrap(a, d, k, fk, hk, hd)
1854	
1855	def Laws.index_wrap(d, hd, k, hk):
1856	  AP.index_wrap.go(d, hd, k, hk)
1857	
1858	def Laws.vector_index_wrap():
1859	  {==}
1860	
1861	# A U32 below 2^d is its own slot (index_of_u32)
1862	
1863	def AP.index_of_u32.go(+d: Nat, +i: U32, hi: {Nat.is_lt(U32.to_nat(i), A.Arrays.slots(d)) == True{} : Bool}) -> {A.Arrays.index(d, i) == U32.to_nat(i) : Nat}:
1864	  %Equal.sym(U32, U32.sub(U32.shln(1, d), 1), U32{AP.lm(32n, d)}, AP.mask_lm(d)) : {U32.to_nat(U32.and(i, _)) == U32.to_nat(i) : Nat}
1865	  %Equal.sym(U32, U32.and(i, U32{AP.lm(32n, d)}), i, AP.u32_and_id(i, d, hi)) : {U32.to_nat(_) == U32.to_nat(i) : Nat}
1866	  {==}
1867	
1868	def Laws.index_of_u32(d, i, hi):
1869	  AP.index_of_u32.go(d, i, hi)
1870	
1871	def Laws.witness_index_wrap():
1872	  {==}