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