1	import Base
2	import ./defs.bend as D
3	import ./proof_base.bend as B
4	import ./proof_tree.bend as P
5	import ./proof_shape.bend as S
6	import ./proof_words.bend as W
7	
8	# The indexing laws. At a node of a perfect tree of depth 1+p, Array.get.go
9	# holds n = 2^(1+p) and an index i below it; h = n >> 1 = 2^p, and z says
10	# i < h: then i goes left unchanged, else right as i - h. So the leaf reached
11	# is leaf i of the list of leaves, and the top level passes i & (n - 1), which
12	# is i modulo 2^d.
13	
14	# One step down
15	# =============
16	
17	law n_half:
18	  for +p: Nat
19	  {Nat.div(Nat.pow(2n, 1n+p), 2n) == Nat.pow(2n, p) : Nat}
20	
21	def n_half(p):
22	  +P = Nat.pow(2n, p)
23	  %Equal.sym(Nat, Nat.mul(2n, P), Nat.mul(P, 2n), W.n_mul_comm(2n, P)) : {Nat.div(_, 2n) == P : Nat}
24	  %B.add_zero(Nat.mul(P, 2n)) : {Nat.div(_, 2n) == P : Nat}
25	  W.n_div_mul_add(P, 2n, 0n, {==})
26	
27	law half:
28	  for +n: U32
29	  for +p: Nat
30	  for +hn: {U32.to_nat(n) == Nat.pow(2n, 1n+p) : Nat}
31	  {U32.to_nat(U32.shr(n)) == Nat.pow(2n, p) : Nat}
32	
33	def half(n, p, hn):
34	  %Equal.sym(Nat, U32.to_nat(U32.shr(n)), Nat.div(U32.to_nat(n), 2n), W.w_shr(n)) :
35	    {_ == Nat.pow(2n, p) : Nat}
36	  %Equal.sym(Nat, U32.to_nat(n), Nat.pow(2n, 1n+p), hn) :
37	    {Nat.div(_, 2n) == Nat.pow(2n, p) : Nat}
38	  n_half(p)
39	
40	law lo_idx:
41	  for +n: U32
42	  for +i: U32
43	  for +p: Nat
44	  for +hn: {U32.to_nat(n) == Nat.pow(2n, 1n+p) : Nat}
45	  for +hz: {U32.is_lt(i, U32.shr(n)) == True{} : Bool}
46	  {Nat.is_lt(U32.to_nat(i), Nat.pow(2n, p)) == True{} : Bool}
47	
48	def lo_idx(n, i, p, hn, hz):
49	  %half(n, p, hn) : {Nat.is_lt(U32.to_nat(i), _) == True{} : Bool}
50	  Equal.trans(Bool, Nat.is_lt(U32.to_nat(i), U32.to_nat(U32.shr(n))), U32.is_lt(i, U32.shr(n)), True{},
51	    Equal.sym(Bool, U32.is_lt(i, U32.shr(n)), Nat.is_lt(U32.to_nat(i), U32.to_nat(U32.shr(n))), W.w_lt(i, U32.shr(n))), hz)
52	
53	law hi_nlt:
54	  for +n: U32
55	  for +i: U32
56	  for +p: Nat
57	  for +hn: {U32.to_nat(n) == Nat.pow(2n, 1n+p) : Nat}
58	  for +hz: {U32.is_lt(i, U32.shr(n)) == False{} : Bool}
59	  {Nat.is_lt(U32.to_nat(i), Nat.pow(2n, p)) == False{} : Bool}
60	
61	def hi_nlt(n, i, p, hn, hz):
62	  %half(n, p, hn) : {Nat.is_lt(U32.to_nat(i), _) == False{} : Bool}
63	  Equal.trans(Bool, Nat.is_lt(U32.to_nat(i), U32.to_nat(U32.shr(n))), U32.is_lt(i, U32.shr(n)), False{},
64	    Equal.sym(Bool, U32.is_lt(i, U32.shr(n)), Nat.is_lt(U32.to_nat(i), U32.to_nat(U32.shr(n))), W.w_lt(i, U32.shr(n))), hz)
65	
66	law le_shr:
67	  for +n: U32
68	  for +i: U32
69	  for +p: Nat
70	  for +hn: {U32.to_nat(n) == Nat.pow(2n, 1n+p) : Nat}
71	  for +hz: {U32.is_lt(i, U32.shr(n)) == False{} : Bool}
72	  {U32.is_le(U32.shr(n), i) == True{} : Bool}
73	
74	def le_shr(n, i, p, hn, hz):
75	  %Equal.sym(Bool, U32.is_le(U32.shr(n), i), Nat.is_le(U32.to_nat(U32.shr(n)), U32.to_nat(i)), W.w_le(U32.shr(n), i)) :
76	    {_ == True{} : Bool}
77	  %Equal.sym(Nat, U32.to_nat(U32.shr(n)), Nat.pow(2n, p), half(n, p, hn)) :
78	    {Nat.is_le(_, U32.to_nat(i)) == True{} : Bool}
79	  B.not_lt_le(U32.to_nat(i), Nat.pow(2n, p), hi_nlt(n, i, p, hn, hz))
80	
81	law hi_sub:
82	  for +n: U32
83	  for +i: U32
84	  for +p: Nat
85	  for +hn: {U32.to_nat(n) == Nat.pow(2n, 1n+p) : Nat}
86	  for +hz: {U32.is_lt(i, U32.shr(n)) == False{} : Bool}
87	  {U32.to_nat(U32.sub(i, U32.shr(n))) == Nat.sub(U32.to_nat(i), Nat.pow(2n, p)) : Nat}
88	
89	def hi_sub(n, i, p, hn, hz):
90	  %Equal.sym(Nat, U32.to_nat(U32.sub(i, U32.shr(n))), Nat.sub(U32.to_nat(i), U32.to_nat(U32.shr(n))),
91	    W.w_sub_le(i, U32.shr(n), le_shr(n, i, p, hn, hz))) :
92	    {_ == Nat.sub(U32.to_nat(i), Nat.pow(2n, p)) : Nat}
93	  %Equal.sym(Nat, U32.to_nat(U32.shr(n)), Nat.pow(2n, p), half(n, p, hn)) :
94	    {Nat.sub(U32.to_nat(i), _) == Nat.sub(U32.to_nat(i), Nat.pow(2n, p)) : Nat}
95	  {==}
96	
97	law hi_idx:
98	  for +n: U32
99	  for +i: U32
100	  for +p: Nat
101	  for +hn: {U32.to_nat(n) == Nat.pow(2n, 1n+p) : Nat}
102	  for +hi: {Nat.is_lt(U32.to_nat(i), Nat.pow(2n, 1n+p)) == True{} : Bool}
103	  for +hz: {U32.is_lt(i, U32.shr(n)) == False{} : Bool}
104	  {Nat.is_lt(U32.to_nat(U32.sub(i, U32.shr(n))), Nat.pow(2n, p)) == True{} : Bool}
105	
106	def hi_idx(n, i, p, hn, hi, hz):
107	  %Equal.sym(Nat, U32.to_nat(U32.sub(i, U32.shr(n))), Nat.sub(U32.to_nat(i), Nat.pow(2n, p)), hi_sub(n, i, p, hn, hz)) :
108	    {Nat.is_lt(_, Nat.pow(2n, p)) == True{} : Bool}
109	  B.lt_sub(Nat.pow(2n, p), U32.to_nat(i), Nat.pow(2n, p), hi_nlt(n, i, p, hn, hz),
110	    B.subst(Nat, X => {Nat.is_lt(U32.to_nat(i), X) == True{} : Bool}, Nat.pow(2n, 1n+p),
111	      Nat.add(Nat.pow(2n, p), Nat.pow(2n, p)), B.pow_succ(p), hi))
112	
113	# Down the tree
114	# =============
115	
116	law gg:
117	  for -T: Data
118	  for +d: Nat
119	  for +t: P.Tree<T>
120	  for +n: U32
121	  for +i: U32
122	  for +z: Bool
123	  for +hf: {D.full(T, P.fromT(T, t), d) == True{} : Bool}
124	  for +hn: {U32.to_nat(n) == Nat.pow(2n, d) : Nat}
125	  for +hi: {Nat.is_lt(U32.to_nat(i), Nat.pow(2n, d)) == True{} : Bool}
126	  for +hz: {U32.is_lt(i, U32.shr(n)) == z : Bool}
127	  {Some{Pair.snd(Array<T>, T, Array.get.go(T, P.fromT(T, t), n, i, z))}
128	    == List.get(&2, T, D.view(T, P.fromT(T, t)), U32.to_nat(i)) : Maybe<&2, T>}
129	
130	def gg(T, d, t, n, i, z, hf, hn, hi, hz):
131	  match d t z:
132	    case 0n P.TLeaf{x} _:
133	      %Equal.sym(Nat, U32.to_nat(i), 0n, B.lt_one(U32.to_nat(i), hi)) :
134	        {Some{x} == List.get(&2, T, [x], _) : Maybe<&2, T>}
135	      {==}
136	    case 0n P.TNode{l, r} _:
137	      Empty.absurd({Some{Pair.snd(Array<T>, T, Array.get.go(T, P.fromT(T, P.TNode{l, r}), n, i, z))}
138	        == List.get(&2, T, D.view(T, P.fromT(T, P.TNode{l, r})), U32.to_nat(i)) : Maybe<&2, T>}, B.false_ne_true(hf))
139	    case 1n+p P.TLeaf{x} _:
140	      Empty.absurd({Some{x} == List.get(&2, T, [x], U32.to_nat(i)) : Maybe<&2, T>}, B.false_ne_true(hf))
141	    case 1n+p P.TNode{l, r} True{}:
142	      +h = U32.shr(n)
143	      +z2 = U32.is_lt(i, U32.shr(h))
144	      +VL = D.view(T, P.fromT(T, l))
145	      +VR = D.view(T, P.fromT(T, r))
146	      +hfl = B.and_true_l(D.full(T, P.fromT(T, l), p), D.full(T, P.fromT(T, r), p), hf)
147	      +lt = lo_idx(n, i, p, hn, hz)
148	      %Equal.sym(T, Pair.snd(Array<T>, T, Array.swap.lo(T, P.fromT(T, r), Array.get.go(T, P.fromT(T, l), h, i, z2))),
149	        Pair.snd(Array<T>, T, Array.get.go(T, P.fromT(T, l), h, i, z2)),
150	        P.lo_snd(T, P.fromT(T, r), Array.get.go(T, P.fromT(T, l), h, i, z2))) :
151	        {Some{_} == List.get(&2, T, List.append(&2, T, VL, VR), U32.to_nat(i)) : Maybe<&2, T>}
152	      %Equal.sym(Maybe<&2, T>, List.get(&2, T, List.append(&2, T, VL, VR), U32.to_nat(i)), List.get(&2, T, VL, U32.to_nat(i)),
153	        B.get_append_l(T, VL, VR, U32.to_nat(i),
154	          B.subst(Nat, X => {Nat.is_lt(U32.to_nat(i), X) == True{} : Bool}, Nat.pow(2n, p), List.length(&2, T, VL),
155	            Equal.sym(Nat, List.length(&2, T, VL), Nat.pow(2n, p), P.view_length(T, p, l, hfl)), lt))) :
156	        {Some{Pair.snd(Array<T>, T, Array.get.go(T, P.fromT(T, l), h, i, z2))} == _ : Maybe<&2, T>}
157	      gg(T, p, l, h, i, z2, hfl, half(n, p, hn), lt, {==})
158	    case 1n+p P.TNode{l, r} False{}:
159	      +h = U32.shr(n)
160	      +j = U32.sub(i, h)
161	      +z2 = U32.is_lt(j, U32.shr(h))
162	      +VL = D.view(T, P.fromT(T, l))
163	      +VR = D.view(T, P.fromT(T, r))
164	      +hfl = B.and_true_l(D.full(T, P.fromT(T, l), p), D.full(T, P.fromT(T, r), p), hf)
165	      +hfr = B.and_true_r(D.full(T, P.fromT(T, l), p), D.full(T, P.fromT(T, r), p), hf)
166	      %Equal.sym(T, Pair.snd(Array<T>, T, Array.swap.hi(T, P.fromT(T, l), Array.get.go(T, P.fromT(T, r), h, j, z2))),
167	        Pair.snd(Array<T>, T, Array.get.go(T, P.fromT(T, r), h, j, z2)),
168	        P.hi_snd(T, P.fromT(T, l), Array.get.go(T, P.fromT(T, r), h, j, z2))) :
169	        {Some{_} == List.get(&2, T, List.append(&2, T, VL, VR), U32.to_nat(i)) : Maybe<&2, T>}
170	      %Equal.sym(Maybe<&2, T>, List.get(&2, T, List.append(&2, T, VL, VR), U32.to_nat(i)),
171	        List.get(&2, T, VR, Nat.sub(U32.to_nat(i), List.length(&2, T, VL))),
172	        B.get_append_r(T, VL, VR, U32.to_nat(i),
173	          B.subst(Nat, X => {Nat.is_lt(U32.to_nat(i), X) == False{} : Bool}, Nat.pow(2n, p), List.length(&2, T, VL),
174	            Equal.sym(Nat, List.length(&2, T, VL), Nat.pow(2n, p), P.view_length(T, p, l, hfl)), hi_nlt(n, i, p, hn, hz)))) :
175	        {Some{Pair.snd(Array<T>, T, Array.get.go(T, P.fromT(T, r), h, j, z2))} == _ : Maybe<&2, T>}
176	      %Equal.sym(Nat, List.length(&2, T, VL), Nat.pow(2n, p), P.view_length(T, p, l, hfl)) :
177	        {Some{Pair.snd(Array<T>, T, Array.get.go(T, P.fromT(T, r), h, j, z2))}
178	          == List.get(&2, T, VR, Nat.sub(U32.to_nat(i), _)) : Maybe<&2, T>}
179	      %hi_sub(n, i, p, hn, hz) :
180	        {Some{Pair.snd(Array<T>, T, Array.get.go(T, P.fromT(T, r), h, j, z2))} == List.get(&2, T, VR, _) : Maybe<&2, T>}
181	      gg(T, p, r, h, j, z2, hfr, half(n, p, hn), hi_idx(n, i, p, hn, hi, hz), {==})
182	
183	# What a swap hands back is the leaf it replaced.
184	law gso:
185	  for -T: Data
186	  for +d: Nat
187	  for +t: P.Tree<T>
188	  for +n: U32
189	  for +i: U32
190	  for +v: T
191	  for +z: Bool
192	  for +hf: {D.full(T, P.fromT(T, t), d) == True{} : Bool}
193	  for +hn: {U32.to_nat(n) == Nat.pow(2n, d) : Nat}
194	  for +hi: {Nat.is_lt(U32.to_nat(i), Nat.pow(2n, d)) == True{} : Bool}
195	  for +hz: {U32.is_lt(i, U32.shr(n)) == z : Bool}
196	  {Some{Pair.snd(Array<T>, T, Array.swap.go(T, P.fromT(T, t), n, i, v, z))}
197	    == List.get(&2, T, D.view(T, P.fromT(T, t)), U32.to_nat(i)) : Maybe<&2, T>}
198	
199	def gso(T, d, t, n, i, v, z, hf, hn, hi, hz):
200	  match d t z:
201	    case 0n P.TLeaf{x} _:
202	      %Equal.sym(Nat, U32.to_nat(i), 0n, B.lt_one(U32.to_nat(i), hi)) :
203	        {Some{x} == List.get(&2, T, [x], _) : Maybe<&2, T>}
204	      {==}
205	    case 0n P.TNode{l, r} _:
206	      Empty.absurd({Some{Pair.snd(Array<T>, T, Array.swap.go(T, P.fromT(T, P.TNode{l, r}), n, i, v, z))}
207	        == List.get(&2, T, D.view(T, P.fromT(T, P.TNode{l, r})), U32.to_nat(i)) : Maybe<&2, T>}, B.false_ne_true(hf))
208	    case 1n+p P.TLeaf{x} _:
209	      Empty.absurd({Some{x} == List.get(&2, T, [x], U32.to_nat(i)) : Maybe<&2, T>}, B.false_ne_true(hf))
210	    case 1n+p P.TNode{l, r} True{}:
211	      +h = U32.shr(n)
212	      +z2 = U32.is_lt(i, U32.shr(h))
213	      +VL = D.view(T, P.fromT(T, l))
214	      +VR = D.view(T, P.fromT(T, r))
215	      +hfl = B.and_true_l(D.full(T, P.fromT(T, l), p), D.full(T, P.fromT(T, r), p), hf)
216	      +lt = lo_idx(n, i, p, hn, hz)
217	      %Equal.sym(T, Pair.snd(Array<T>, T, Array.swap.lo(T, P.fromT(T, r), Array.swap.go(T, P.fromT(T, l), h, i, v, z2))),
218	        Pair.snd(Array<T>, T, Array.swap.go(T, P.fromT(T, l), h, i, v, z2)),
219	        P.lo_snd(T, P.fromT(T, r), Array.swap.go(T, P.fromT(T, l), h, i, v, z2))) :
220	        {Some{_} == List.get(&2, T, List.append(&2, T, VL, VR), U32.to_nat(i)) : Maybe<&2, T>}
221	      %Equal.sym(Maybe<&2, T>, List.get(&2, T, List.append(&2, T, VL, VR), U32.to_nat(i)), List.get(&2, T, VL, U32.to_nat(i)),
222	        B.get_append_l(T, VL, VR, U32.to_nat(i),
223	          B.subst(Nat, X => {Nat.is_lt(U32.to_nat(i), X) == True{} : Bool}, Nat.pow(2n, p), List.length(&2, T, VL),
224	            Equal.sym(Nat, List.length(&2, T, VL), Nat.pow(2n, p), P.view_length(T, p, l, hfl)), lt))) :
225	        {Some{Pair.snd(Array<T>, T, Array.swap.go(T, P.fromT(T, l), h, i, v, z2))} == _ : Maybe<&2, T>}
226	      gso(T, p, l, h, i, v, z2, hfl, half(n, p, hn), lt, {==})
227	    case 1n+p P.TNode{l, r} False{}:
228	      +h = U32.shr(n)
229	      +j = U32.sub(i, h)
230	      +z2 = U32.is_lt(j, U32.shr(h))
231	      +VL = D.view(T, P.fromT(T, l))
232	      +VR = D.view(T, P.fromT(T, r))
233	      +hfl = B.and_true_l(D.full(T, P.fromT(T, l), p), D.full(T, P.fromT(T, r), p), hf)
234	      +hfr = B.and_true_r(D.full(T, P.fromT(T, l), p), D.full(T, P.fromT(T, r), p), hf)
235	      %Equal.sym(T, Pair.snd(Array<T>, T, Array.swap.hi(T, P.fromT(T, l), Array.swap.go(T, P.fromT(T, r), h, j, v, z2))),
236	        Pair.snd(Array<T>, T, Array.swap.go(T, P.fromT(T, r), h, j, v, z2)),
237	        P.hi_snd(T, P.fromT(T, l), Array.swap.go(T, P.fromT(T, r), h, j, v, z2))) :
238	        {Some{_} == List.get(&2, T, List.append(&2, T, VL, VR), U32.to_nat(i)) : Maybe<&2, T>}
239	      %Equal.sym(Maybe<&2, T>, List.get(&2, T, List.append(&2, T, VL, VR), U32.to_nat(i)),
240	        List.get(&2, T, VR, Nat.sub(U32.to_nat(i), List.length(&2, T, VL))),
241	        B.get_append_r(T, VL, VR, U32.to_nat(i),
242	          B.subst(Nat, X => {Nat.is_lt(U32.to_nat(i), X) == False{} : Bool}, Nat.pow(2n, p), List.length(&2, T, VL),
243	            Equal.sym(Nat, List.length(&2, T, VL), Nat.pow(2n, p), P.view_length(T, p, l, hfl)), hi_nlt(n, i, p, hn, hz)))) :
244	        {Some{Pair.snd(Array<T>, T, Array.swap.go(T, P.fromT(T, r), h, j, v, z2))} == _ : Maybe<&2, T>}
245	      %Equal.sym(Nat, List.length(&2, T, VL), Nat.pow(2n, p), P.view_length(T, p, l, hfl)) :
246	        {Some{Pair.snd(Array<T>, T, Array.swap.go(T, P.fromT(T, r), h, j, v, z2))}
247	          == List.get(&2, T, VR, Nat.sub(U32.to_nat(i), _)) : Maybe<&2, T>}
248	      %hi_sub(n, i, p, hn, hz) :
249	        {Some{Pair.snd(Array<T>, T, Array.swap.go(T, P.fromT(T, r), h, j, v, z2))} == List.get(&2, T, VR, _) : Maybe<&2, T>}
250	      gso(T, p, r, h, j, v, z2, hfr, half(n, p, hn), hi_idx(n, i, p, hn, hi, hz), {==})
251	
252	# A swap writes leaf i of the list of leaves.
253	law gsv:
254	  for -T: Data
255	  for +d: Nat
256	  for +t: P.Tree<T>
257	  for +n: U32
258	  for +i: U32
259	  for +v: T
260	  for +z: Bool
261	  for +hf: {D.full(T, P.fromT(T, t), d) == True{} : Bool}
262	  for +hn: {U32.to_nat(n) == Nat.pow(2n, d) : Nat}
263	  for +hi: {Nat.is_lt(U32.to_nat(i), Nat.pow(2n, d)) == True{} : Bool}
264	  for +hz: {U32.is_lt(i, U32.shr(n)) == z : Bool}
265	  {D.view(T, Pair.fst(Array<T>, T, Array.swap.go(T, P.fromT(T, t), n, i, v, z)))
266	    == List.set(&2, T, D.view(T, P.fromT(T, t)), U32.to_nat(i), v) : List<&2, T>}
267	
268	def gsv(T, d, t, n, i, v, z, hf, hn, hi, hz):
269	  match d t z:
270	    case 0n P.TLeaf{x} _:
271	      %Equal.sym(Nat, U32.to_nat(i), 0n, B.lt_one(U32.to_nat(i), hi)) :
272	        {[v] == List.set(&2, T, [x], _, v) : List<&2, T>}
273	      {==}
274	    case 0n P.TNode{l, r} _:
275	      Empty.absurd({D.view(T, Pair.fst(Array<T>, T, Array.swap.go(T, P.fromT(T, P.TNode{l, r}), n, i, v, z)))
276	        == List.set(&2, T, D.view(T, P.fromT(T, P.TNode{l, r})), U32.to_nat(i), v) : List<&2, T>}, B.false_ne_true(hf))
277	    case 1n+p P.TLeaf{x} _:
278	      Empty.absurd({[v] == List.set(&2, T, [x], U32.to_nat(i), v) : List<&2, T>}, B.false_ne_true(hf))
279	    case 1n+p P.TNode{l, r} True{}:
280	      +h = U32.shr(n)
281	      +z2 = U32.is_lt(i, U32.shr(h))
282	      +VL = D.view(T, P.fromT(T, l))
283	      +VR = D.view(T, P.fromT(T, r))
284	      +hfl = B.and_true_l(D.full(T, P.fromT(T, l), p), D.full(T, P.fromT(T, r), p), hf)
285	      +lt = lo_idx(n, i, p, hn, hz)
286	      %Equal.sym(Array<T>, Pair.fst(Array<T>, T, Array.swap.lo(T, P.fromT(T, r), Array.swap.go(T, P.fromT(T, l), h, i, v, z2))),
287	        ANode{Pair.fst(Array<T>, T, Array.swap.go(T, P.fromT(T, l), h, i, v, z2)), P.fromT(T, r)},
288	        P.lo_fst(T, P.fromT(T, r), Array.swap.go(T, P.fromT(T, l), h, i, v, z2))) :
289	        {D.view(T, _) == List.set(&2, T, List.append(&2, T, VL, VR), U32.to_nat(i), v) : List<&2, T>}
290	      %Equal.sym(List<&2, T>, List.set(&2, T, List.append(&2, T, VL, VR), U32.to_nat(i), v),
291	        List.append(&2, T, List.set(&2, T, VL, U32.to_nat(i), v), VR),
292	        B.set_append_l(T, VL, VR, U32.to_nat(i), v,
293	          B.subst(Nat, X => {Nat.is_lt(U32.to_nat(i), X) == True{} : Bool}, Nat.pow(2n, p), List.length(&2, T, VL),
294	            Equal.sym(Nat, List.length(&2, T, VL), Nat.pow(2n, p), P.view_length(T, p, l, hfl)), lt))) :
295	        {List.append(&2, T, D.view(T, Pair.fst(Array<T>, T, Array.swap.go(T, P.fromT(T, l), h, i, v, z2))), VR) == _ : List<&2, T>}
296	      %gsv(T, p, l, h, i, v, z2, hfl, half(n, p, hn), lt, {==}) :
297	        {List.append(&2, T, D.view(T, Pair.fst(Array<T>, T, Array.swap.go(T, P.fromT(T, l), h, i, v, z2))), VR)
298	          == List.append(&2, T, _, VR) : List<&2, T>}
299	      {==}
300	    case 1n+p P.TNode{l, r} False{}:
301	      +h = U32.shr(n)
302	      +j = U32.sub(i, h)
303	      +z2 = U32.is_lt(j, U32.shr(h))
304	      +VL = D.view(T, P.fromT(T, l))
305	      +VR = D.view(T, P.fromT(T, r))
306	      +hfl = B.and_true_l(D.full(T, P.fromT(T, l), p), D.full(T, P.fromT(T, r), p), hf)
307	      +hfr = B.and_true_r(D.full(T, P.fromT(T, l), p), D.full(T, P.fromT(T, r), p), hf)
308	      %Equal.sym(Array<T>, Pair.fst(Array<T>, T, Array.swap.hi(T, P.fromT(T, l), Array.swap.go(T, P.fromT(T, r), h, j, v, z2))),
309	        ANode{P.fromT(T, l), Pair.fst(Array<T>, T, Array.swap.go(T, P.fromT(T, r), h, j, v, z2))},
310	        P.hi_fst(T, P.fromT(T, l), Array.swap.go(T, P.fromT(T, r), h, j, v, z2))) :
311	        {D.view(T, _) == List.set(&2, T, List.append(&2, T, VL, VR), U32.to_nat(i), v) : List<&2, T>}
312	      %Equal.sym(List<&2, T>, List.set(&2, T, List.append(&2, T, VL, VR), U32.to_nat(i), v),
313	        List.append(&2, T, VL, List.set(&2, T, VR, Nat.sub(U32.to_nat(i), List.length(&2, T, VL)), v)),
314	        B.set_append_r(T, VL, VR, U32.to_nat(i), v,
315	          B.subst(Nat, X => {Nat.is_lt(U32.to_nat(i), X) == False{} : Bool}, Nat.pow(2n, p), List.length(&2, T, VL),
316	            Equal.sym(Nat, List.length(&2, T, VL), Nat.pow(2n, p), P.view_length(T, p, l, hfl)), hi_nlt(n, i, p, hn, hz)))) :
317	        {List.append(&2, T, VL, D.view(T, Pair.fst(Array<T>, T, Array.swap.go(T, P.fromT(T, r), h, j, v, z2)))) == _ : List<&2, T>}
318	      %Equal.sym(Nat, List.length(&2, T, VL), Nat.pow(2n, p), P.view_length(T, p, l, hfl)) :
319	        {List.append(&2, T, VL, D.view(T, Pair.fst(Array<T>, T, Array.swap.go(T, P.fromT(T, r), h, j, v, z2))))
320	          == List.append(&2, T, VL, List.set(&2, T, VR, Nat.sub(U32.to_nat(i), _), v)) : List<&2, T>}
321	      %hi_sub(n, i, p, hn, hz) :
322	        {List.append(&2, T, VL, D.view(T, Pair.fst(Array<T>, T, Array.swap.go(T, P.fromT(T, r), h, j, v, z2))))
323	          == List.append(&2, T, VL, List.set(&2, T, VR, _, v)) : List<&2, T>}
324	      %gsv(T, p, r, h, j, v, z2, hfr, half(n, p, hn), hi_idx(n, i, p, hn, hi, hz), {==}) :
325	        {List.append(&2, T, VL, D.view(T, Pair.fst(Array<T>, T, Array.swap.go(T, P.fromT(T, r), h, j, v, z2))))
326	          == List.append(&2, T, VL, _) : List<&2, T>}
327	      {==}
328	
329	# The top level: size 2^d and index i & (2^d - 1)
330	# ===============================================
331	
332	law one_mul:
333	  for +x: Nat
334	  {Nat.mul(U32.to_nat(1), x) == x : Nat}
335	
336	def one_mul(x):
337	  B.add_zero(x)
338	
339	law size_n:
340	  for +d: Nat
341	  for +hd: {Nat.is_lt(d, 32n) == True{} : Bool}
342	  {U32.to_nat(U32.shln(1, d)) == Nat.pow(2n, d) : Nat}
343	
344	def size_n(d, hd):
345	  +fits = B.subst(Nat, X => {Nat.is_lt(X, Nat.pow(2n, 32n)) == True{} : Bool},
346	    Nat.pow(2n, d), Nat.mul(U32.to_nat(1), Nat.pow(2n, d)),
347	    Equal.sym(Nat, Nat.mul(U32.to_nat(1), Nat.pow(2n, d)), Nat.pow(2n, d), one_mul(Nat.pow(2n, d))),
348	    B.pow_lt(d, 32n, hd))
349	  %Equal.sym(Nat, U32.to_nat(U32.shln(1, d)), Nat.mul(U32.to_nat(1), Nat.pow(2n, d)), W.w_shln_fits(1, d, fits)) :
350	    {_ == Nat.pow(2n, d) : Nat}
351	  one_mul(Nat.pow(2n, d))
352	
353	law le0:
354	  for +y: Nat
355	  {Nat.is_le(0n, y) == True{} : Bool}
356	
357	def le0(y):
358	  match y:
359	    case 0n:
360	      {==}
361	    case 1n+k:
362	      {==}
363	
364	law le1_pow:
365	  for +d: Nat
366	  {Nat.is_le(1n, Nat.pow(2n, d)) == True{} : Bool}
367	
368	def le1_pow.go(+x: Nat, h: {Nat.is_lt(0n, x) == True{} : Bool}) -> {Nat.is_le(1n, x) == True{} : Bool}:
369	  match x:
370	    case 0n:
371	      Empty.absurd({Nat.is_le(1n, 0n) == True{} : Bool}, B.false_ne_true(h))
372	    case 1n+y:
373	      le0(y)
374	
375	def le1_pow(d):
376	  le1_pow.go(Nat.pow(2n, d), B.pow_pos(d))
377	
378	law le1:
379	  for +d: Nat
380	  for +hd: {Nat.is_lt(d, 32n) == True{} : Bool}
381	  {U32.is_le(1, U32.shln(1, d)) == True{} : Bool}
382	
383	def le1(d, hd):
384	  +S = U32.shln(1, d)
385	  %Equal.sym(Bool, U32.is_le(1, S), Nat.is_le(U32.to_nat(1), U32.to_nat(S)), W.w_le(1, S)) :
386	    {_ == True{} : Bool}
387	  %Equal.sym(Nat, U32.to_nat(S), Nat.pow(2n, d), size_n(d, hd)) :
388	    {Nat.is_le(U32.to_nat(1), _) == True{} : Bool}
389	  le1_pow(d)
390	
391	law mask_n:
392	  for +d: Nat
393	  for +hd: {Nat.is_lt(d, 32n) == True{} : Bool}
394	  {U32.to_nat(U32.sub(U32.shln(1, d), 1)) == Nat.sub(Nat.pow(2n, d), 1n) : Nat}
395	
396	def mask_n(d, hd):
397	  +S = U32.shln(1, d)
398	  %Equal.sym(Nat, U32.to_nat(U32.sub(S, 1)), Nat.sub(U32.to_nat(S), U32.to_nat(1)), W.w_sub_le(S, 1, le1(d, hd))) :
399	    {_ == Nat.sub(Nat.pow(2n, d), 1n) : Nat}
400	  %Equal.sym(Nat, U32.to_nat(S), Nat.pow(2n, d), size_n(d, hd)) :
401	    {Nat.sub(_, U32.to_nat(1)) == Nat.sub(Nat.pow(2n, d), 1n) : Nat}
402	  {==}
403	
404	law slot_n:
405	  for +i: U32
406	  for +d: Nat
407	  for +hd: {Nat.is_lt(d, 32n) == True{} : Bool}
408	  {U32.to_nat(U32.and(i, U32.sub(U32.shln(1, d), 1))) == D.slot(i, d) : Nat}
409	
410	def slot_n(i, d, hd):
411	  W.w_and_mask(i, U32.sub(U32.shln(1, d), 1), d, mask_n(d, hd))
412	
413	law slot_lt_t:
414	  for +i: U32
415	  for +d: Nat
416	  {Nat.is_lt(D.slot(i, d), Nat.pow(2n, d)) == True{} : Bool}
417	
418	def slot_lt_t(i, d):
419	  W.n_mod_lt(U32.to_nat(i), Nat.pow(2n, d), B.pow_pos(d))
420	
421	law slot_small_t:
422	  for +i: U32
423	  for +d: Nat
424	  for +h: {Nat.is_lt(U32.to_nat(i), Nat.pow(2n, d)) == True{} : Bool}
425	  {D.slot(i, d) == U32.to_nat(i) : Nat}
426	
427	def slot_small_t(i, d, h):
428	  W.n_mod_small(U32.to_nat(i), Nat.pow(2n, d), h)
429	
430	law jlt:
431	  for +i: U32
432	  for +d: Nat
433	  for +hd: {Nat.is_lt(d, 32n) == True{} : Bool}
434	  {Nat.is_lt(U32.to_nat(U32.and(i, U32.sub(U32.shln(1, d), 1))), Nat.pow(2n, d)) == True{} : Bool}
435	
436	def jlt(i, d, hd):
437	  B.subst(Nat, X => {Nat.is_lt(X, Nat.pow(2n, d)) == True{} : Bool}, D.slot(i, d),
438	    U32.to_nat(U32.and(i, U32.sub(U32.shln(1, d), 1))),
439	    Equal.sym(Nat, U32.to_nat(U32.and(i, U32.sub(U32.shln(1, d), 1))), D.slot(i, d), slot_n(i, d, hd)),
440	    slot_lt_t(i, d))
441	
442	# The laws, for a mirrored array
443	# ==============================
444	
445	law size_count_t:
446	  for -T: Data
447	  for +t: P.Tree<T>
448	  for +d: Nat
449	  for +hf: {D.full(T, P.fromT(T, t), d) == True{} : Bool}
450	  for +hd: {Nat.is_lt(d, 32n) == True{} : Bool}
451	  {U32.to_nat(Pair.snd(Array<T>, U32, Array.size(T, P.fromT(T, t)))) == Nat.pow(2n, d) : Nat}
452	
453	def size_count_t(T, t, d, hf, hd):
454	  %Equal.sym(Array<T> & U32, Array.size(T, P.fromT(T, t)), (P.fromT(T, t), U32.shln(1, d)), P.size_tree(T, d, t, hf)) :
455	    {U32.to_nat(Pair.snd(Array<T>, U32, _)) == Nat.pow(2n, d) : Nat}
456	  size_n(d, hd)
457	
458	law get_view_t:
459	  for -T: Data
460	  for +t: P.Tree<T>
461	  for +d: Nat
462	  for +i: U32
463	  for +hf: {D.full(T, P.fromT(T, t), d) == True{} : Bool}
464	  for +hd: {Nat.is_lt(d, 32n) == True{} : Bool}
465	  {Some{Pair.snd(Array<T>, T, Array.get(T, P.fromT(T, t), i))}
466	    == List.get(&2, T, D.view(T, P.fromT(T, t)), D.slot(i, d)) : Maybe<&2, T>}
467	
468	def get_view_t(T, t, d, i, hf, hd):
469	  +S = U32.shln(1, d)
470	  +j = U32.and(i, U32.sub(S, 1))
471	  +z = U32.is_lt(j, U32.shr(S))
472	  %Equal.sym(Array<T> & U32, Array.size(T, P.fromT(T, t)), (P.fromT(T, t), S), P.size_tree(T, d, t, hf)) :
473	    {Some{Pair.snd(Array<T>, T, Array.get.at(T, i, _))} == List.get(&2, T, D.view(T, P.fromT(T, t)), D.slot(i, d)) : Maybe<&2, T>}
474	  %slot_n(i, d, hd) :
475	    {Some{Pair.snd(Array<T>, T, Array.get.go(T, P.fromT(T, t), S, j, z))} == List.get(&2, T, D.view(T, P.fromT(T, t)), _) : Maybe<&2, T>}
476	  gg(T, d, t, S, j, z, hf, size_n(d, hd), jlt(i, d, hd), {==})
477	
478	law swap_old_t:
479	  for -T: Data
480	  for +t: P.Tree<T>
481	  for +d: Nat
482	  for +i: U32
483	  for +v: T
484	  for +hf: {D.full(T, P.fromT(T, t), d) == True{} : Bool}
485	  for +hd: {Nat.is_lt(d, 32n) == True{} : Bool}
486	  {Some{Pair.snd(Array<T>, T, Array.swap(T, P.fromT(T, t), i, v))}
487	    == List.get(&2, T, D.view(T, P.fromT(T, t)), D.slot(i, d)) : Maybe<&2, T>}
488	
489	def swap_old_t(T, t, d, i, v, hf, hd):
490	  +S = U32.shln(1, d)
491	  +j = U32.and(i, U32.sub(S, 1))
492	  +z = U32.is_lt(j, U32.shr(S))
493	  %Equal.sym(Array<T> & U32, Array.size(T, P.fromT(T, t)), (P.fromT(T, t), S), P.size_tree(T, d, t, hf)) :
494	    {Some{Pair.snd(Array<T>, T, Array.swap.at(T, i, v, _))} == List.get(&2, T, D.view(T, P.fromT(T, t)), D.slot(i, d)) : Maybe<&2, T>}
495	  %slot_n(i, d, hd) :
496	    {Some{Pair.snd(Array<T>, T, Array.swap.go(T, P.fromT(T, t), S, j, v, z))} == List.get(&2, T, D.view(T, P.fromT(T, t)), _) : Maybe<&2, T>}
497	  gso(T, d, t, S, j, v, z, hf, size_n(d, hd), jlt(i, d, hd), {==})
498	
499	law swap_view_t:
500	  for -T: Data
501	  for +t: P.Tree<T>
502	  for +d: Nat
503	  for +i: U32
504	  for +v: T
505	  for +hf: {D.full(T, P.fromT(T, t), d) == True{} : Bool}
506	  for +hd: {Nat.is_lt(d, 32n) == True{} : Bool}
507	  {D.view(T, Pair.fst(Array<T>, T, Array.swap(T, P.fromT(T, t), i, v)))
508	    == List.set(&2, T, D.view(T, P.fromT(T, t)), D.slot(i, d), v) : List<&2, T>}
509	
510	def swap_view_t(T, t, d, i, v, hf, hd):
511	  +S = U32.shln(1, d)
512	  +j = U32.and(i, U32.sub(S, 1))
513	  +z = U32.is_lt(j, U32.shr(S))
514	  %Equal.sym(Array<T> & U32, Array.size(T, P.fromT(T, t)), (P.fromT(T, t), S), P.size_tree(T, d, t, hf)) :
515	    {D.view(T, Pair.fst(Array<T>, T, Array.swap.at(T, i, v, _))) == List.set(&2, T, D.view(T, P.fromT(T, t)), D.slot(i, d), v) : List<&2, T>}
516	  %slot_n(i, d, hd) :
517	    {D.view(T, Pair.fst(Array<T>, T, Array.swap.go(T, P.fromT(T, t), S, j, v, z))) == List.set(&2, T, D.view(T, P.fromT(T, t)), _, v) : List<&2, T>}
518	  gsv(T, d, t, S, j, v, z, hf, size_n(d, hd), jlt(i, d, hd), {==})
519	
520	law set_view_t:
521	  for -T: Data
522	  for +t: P.Tree<T>
523	  for +d: Nat
524	  for +i: U32
525	  for +v: T
526	  for +hf: {D.full(T, P.fromT(T, t), d) == True{} : Bool}
527	  for +hd: {Nat.is_lt(d, 32n) == True{} : Bool}
528	  {D.view(T, Array.set(T, P.fromT(T, t), i, v))
529	    == List.set(&2, T, D.view(T, P.fromT(T, t)), D.slot(i, d), v) : List<&2, T>}
530	
531	def set_view_t(T, t, d, i, v, hf, hd):
532	  +S = U32.shln(1, d)
533	  +j = U32.and(i, U32.sub(S, 1))
534	  +z = U32.is_lt(j, U32.shr(S))
535	  %Equal.sym(Array<T> & U32, Array.size(T, P.fromT(T, t)), (P.fromT(T, t), S), P.size_tree(T, d, t, hf)) :
536	    {D.view(T, Array.set.fin(T, Array.swap.at(T, i, v, _))) == List.set(&2, T, D.view(T, P.fromT(T, t)), D.slot(i, d), v) : List<&2, T>}
537	  %Equal.sym(Array<T>, Array.set.fin(T, Array.swap.go(T, P.fromT(T, t), S, j, v, z)),
538	    Pair.fst(Array<T>, T, Array.swap.go(T, P.fromT(T, t), S, j, v, z)), P.fin_fst(T, Array.swap.go(T, P.fromT(T, t), S, j, v, z))) :
539	    {D.view(T, _) == List.set(&2, T, D.view(T, P.fromT(T, t)), D.slot(i, d), v) : List<&2, T>}
540	  %slot_n(i, d, hd) :
541	    {D.view(T, Pair.fst(Array<T>, T, Array.swap.go(T, P.fromT(T, t), S, j, v, z))) == List.set(&2, T, D.view(T, P.fromT(T, t)), _, v) : List<&2, T>}
542	  gsv(T, d, t, S, j, v, z, hf, size_n(d, hd), jlt(i, d, hd), {==})
543	
544	# Writing one leaf, then reading another
545	# ======================================
546	
547	# The tree a swap leaves, as a Tree (so the written array has a mirror too).
548	def tswap(-T: Data, t: P.Tree<T>, +n: U32, +i: U32, v: T, z: Bool) -> P.Tree<T>:
549	  match t z:
550	    case P.TLeaf{x} _:
551	      P.TLeaf{v}
552	    case P.TNode{l, r} True{}:
553	      +h = U32.shr(n)
554	      P.TNode{tswap(T, l, h, i, v, U32.is_lt(i, U32.shr(h))), r}
555	    case P.TNode{l, r} False{}:
556	      +h = U32.shr(n)
557	      +j = U32.sub(i, h)
558	      P.TNode{l, tswap(T, r, h, j, v, U32.is_lt(j, U32.shr(h)))}
559	
560	law tswap_eq:
561	  for -T: Data
562	  for +t: P.Tree<T>
563	  for +n: U32
564	  for +i: U32
565	  for +v: T
566	  for +z: Bool
567	  {P.fromT(T, tswap(T, t, n, i, v, z)) == Pair.fst(Array<T>, T, Array.swap.go(T, P.fromT(T, t), n, i, v, z)) : Array<T>}
568	
569	def tswap_eq(T, t, n, i, v, z):
570	  match t z:
571	    case P.TLeaf{x} _:
572	      {==}
573	    case P.TNode{l, r} True{}:
574	      +h = U32.shr(n)
575	      +z2 = U32.is_lt(i, U32.shr(h))
576	      %Equal.sym(Array<T>, Pair.fst(Array<T>, T, Array.swap.lo(T, P.fromT(T, r), Array.swap.go(T, P.fromT(T, l), h, i, v, z2))),
577	        ANode{Pair.fst(Array<T>, T, Array.swap.go(T, P.fromT(T, l), h, i, v, z2)), P.fromT(T, r)},
578	        P.lo_fst(T, P.fromT(T, r), Array.swap.go(T, P.fromT(T, l), h, i, v, z2))) :
579	        {ANode{P.fromT(T, tswap(T, l, h, i, v, z2)), P.fromT(T, r)} == _ : Array<T>}
580	      %tswap_eq(T, l, h, i, v, z2) :
581	        {ANode{P.fromT(T, tswap(T, l, h, i, v, z2)), P.fromT(T, r)} == ANode{_, P.fromT(T, r)} : Array<T>}
582	      {==}
583	    case P.TNode{l, r} False{}:
584	      +h = U32.shr(n)
585	      +j = U32.sub(i, h)
586	      +z2 = U32.is_lt(j, U32.shr(h))
587	      %Equal.sym(Array<T>, Pair.fst(Array<T>, T, Array.swap.hi(T, P.fromT(T, l), Array.swap.go(T, P.fromT(T, r), h, j, v, z2))),
588	        ANode{P.fromT(T, l), Pair.fst(Array<T>, T, Array.swap.go(T, P.fromT(T, r), h, j, v, z2))},
589	        P.hi_fst(T, P.fromT(T, l), Array.swap.go(T, P.fromT(T, r), h, j, v, z2))) :
590	        {ANode{P.fromT(T, l), P.fromT(T, tswap(T, r, h, j, v, z2))} == _ : Array<T>}
591	      %tswap_eq(T, r, h, j, v, z2) :
592	        {ANode{P.fromT(T, l), P.fromT(T, tswap(T, r, h, j, v, z2))} == ANode{P.fromT(T, l), _} : Array<T>}
593	      {==}
594	
595	def set_tree(-T: Data, +t: P.Tree<T>, +i: U32, +v: T) -> P.Tree<T>:
596	  +n = Pair.snd(Array<T>, U32, Array.size(T, P.fromT(T, t)))
597	  +j = U32.and(i, U32.sub(n, 1))
598	  tswap(T, t, n, j, v, U32.is_lt(j, U32.shr(n)))
599	
600	law set_tree_eq:
601	  for -T: Data
602	  for +t: P.Tree<T>
603	  for +i: U32
604	  for +v: T
605	  {Array.set(T, P.fromT(T, t), i, v) == P.fromT(T, set_tree(T, t, i, v)) : Array<T>}
606	
607	def set_tree_eq(T, t, i, v):
608	  +n = Pair.snd(Array<T>, U32, Array.size(T, P.fromT(T, t)))
609	  +j = U32.and(i, U32.sub(n, 1))
610	  +z = U32.is_lt(j, U32.shr(n))
611	  %Equal.sym(Array<T> & U32, Array.size(T, P.fromT(T, t)), (P.fromT(T, t), n), P.size_eta(T, P.fromT(T, t))) :
612	    {Array.set.fin(T, Array.swap.at(T, i, v, _)) == P.fromT(T, set_tree(T, t, i, v)) : Array<T>}
613	  %Equal.sym(Array<T>, Array.set.fin(T, Array.swap.go(T, P.fromT(T, t), n, j, v, z)),
614	    Pair.fst(Array<T>, T, Array.swap.go(T, P.fromT(T, t), n, j, v, z)), P.fin_fst(T, Array.swap.go(T, P.fromT(T, t), n, j, v, z))) :
615	    {_ == P.fromT(T, set_tree(T, t, i, v)) : Array<T>}
616	  Equal.sym(Array<T>, P.fromT(T, tswap(T, t, n, j, v, z)), Pair.fst(Array<T>, T, Array.swap.go(T, P.fromT(T, t), n, j, v, z)),
617	    tswap_eq(T, t, n, j, v, z))
618	
619	def unsome(-T: Data, +d: T, m: Maybe<&2, T>) -> T:
620	  match m:
621	    case None{}:
622	      d
623	    case Some{x}:
624	      x
625	
626	law get_set_other_t:
627	  for -T: Data
628	  for +t: P.Tree<T>
629	  for +d: Nat
630	  for +i: U32
631	  for +j: U32
632	  for +v: T
633	  for +hf: {D.full(T, P.fromT(T, t), d) == True{} : Bool}
634	  for +hd: {Nat.is_lt(d, 32n) == True{} : Bool}
635	  for +hij: {Nat.is_eq(D.slot(i, d), D.slot(j, d)) == False{} : Bool}
636	  {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, P.fromT(T, t), i, v), j))
637	    == Pair.snd(Array<T>, T, Array.get(T, P.fromT(T, t), j)) : T}
638	
639	def get_set_other_t(T, t, d, i, j, v, hf, hd, hij):
640	  +t2 = set_tree(T, t, i, v)
641	  +V = D.view(T, P.fromT(T, t))
642	  +se = set_tree_eq(T, t, i, v)
643	  +hf2 = B.subst(Array<T>, X => {D.full(T, X, d) == True{} : Bool}, Array.set(T, P.fromT(T, t), i, v), P.fromT(T, t2), se,
644	    S.set_full(T, P.fromT(T, t), d, i, v, hf))
645	  +c1 = get_view_t(T, t2, d, j, hf2, hd)
646	  +c2 = Equal.trans(List<&2, T>, D.view(T, P.fromT(T, t2)), D.view(T, Array.set(T, P.fromT(T, t), i, v)),
647	    List.set(&2, T, V, D.slot(i, d), v),
648	    Equal.cong(Array<T>, List<&2, T>, X => D.view(T, X), P.fromT(T, t2), Array.set(T, P.fromT(T, t), i, v),
649	      Equal.sym(Array<T>, Array.set(T, P.fromT(T, t), i, v), P.fromT(T, t2), se)),
650	    set_view_t(T, t, d, i, v, hf, hd))
651	  +c3 = B.get_set_ne(T, V, D.slot(i, d), D.slot(j, d), v, hij)
652	  +c4 = Equal.sym(Maybe<&2, T>, Some{Pair.snd(Array<T>, T, Array.get(T, P.fromT(T, t), j))},
653	    List.get(&2, T, V, D.slot(j, d)), get_view_t(T, t, d, j, hf, hd))
654	  +ss = Equal.trans(Maybe<&2, T>, Some{Pair.snd(Array<T>, T, Array.get(T, P.fromT(T, t2), j))},
655	    List.get(&2, T, D.view(T, P.fromT(T, t2)), D.slot(j, d)), Some{Pair.snd(Array<T>, T, Array.get(T, P.fromT(T, t), j))},
656	    c1,
657	    Equal.trans(Maybe<&2, T>, List.get(&2, T, D.view(T, P.fromT(T, t2)), D.slot(j, d)),
658	      List.get(&2, T, List.set(&2, T, V, D.slot(i, d), v), D.slot(j, d)),
659	      Some{Pair.snd(Array<T>, T, Array.get(T, P.fromT(T, t), j))},
660	      Equal.cong(List<&2, T>, Maybe<&2, T>, X => List.get(&2, T, X, D.slot(j, d)),
661	        D.view(T, P.fromT(T, t2)), List.set(&2, T, V, D.slot(i, d), v), c2),
662	      Equal.trans(Maybe<&2, T>, List.get(&2, T, List.set(&2, T, V, D.slot(i, d), v), D.slot(j, d)),
663	        List.get(&2, T, V, D.slot(j, d)), Some{Pair.snd(Array<T>, T, Array.get(T, P.fromT(T, t), j))}, c3, c4)))
664	  %Equal.sym(Array<T>, Array.set(T, P.fromT(T, t), i, v), P.fromT(T, t2), se) :
665	    {Pair.snd(Array<T>, T, Array.get(T, _, j)) == Pair.snd(Array<T>, T, Array.get(T, P.fromT(T, t), j)) : T}
666	  Equal.cong(Maybe<&2, T>, T, m => unsome(T, v, m), Some{Pair.snd(Array<T>, T, Array.get(T, P.fromT(T, t2), j))},
667	    Some{Pair.snd(Array<T>, T, Array.get(T, P.fromT(T, t), j))}, ss)