proof_index.bend

lawful-arrays@0.1.0.0 · 667 lines · 32 definitions

1import Base
2import lawful-arrays@0.1.0.0/defs.bend as D
3import lawful-arrays@0.1.0.0/proof_base.bend as B
4import lawful-arrays@0.1.0.0/proof_tree.bend as P
5import lawful-arrays@0.1.0.0/proof_shape.bend as S
6import lawful-arrays@0.1.0.0/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
17law n_half:
18  for +p: Nat
19  {Nat.div(Nat.pow(2n, 1n+p), 2n) == Nat.pow(2n, p) : Nat}
20
21def 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
27law 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
33def 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
40law 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
48def 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
53law 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
61def 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
66law 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
74def 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
81law 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
89def 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
97law 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
106def 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
116law 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
130def 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.
184law 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
199def 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.
253law 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
268def 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
332law one_mul:
333  for +x: Nat
334  {Nat.mul(U32.to_nat(1), x) == x : Nat}
335
336def one_mul(x):
337  B.add_zero(x)
338
339law 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
344def 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
353law le0:
354  for +y: Nat
355  {Nat.is_le(0n, y) == True{} : Bool}
356
357def le0(y):
358  match y:
359    case 0n:
360      {==}
361    case 1n+k:
362      {==}
363
364law le1_pow:
365  for +d: Nat
366  {Nat.is_le(1n, Nat.pow(2n, d)) == True{} : Bool}
367
368def 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
375def le1_pow(d):
376  le1_pow.go(Nat.pow(2n, d), B.pow_pos(d))
377
378law 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
383def 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
391law 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
396def 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
404law 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
410def slot_n(i, d, hd):
411  W.w_and_mask(i, U32.sub(U32.shln(1, d), 1), d, mask_n(d, hd))
412
413law 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
418def slot_lt_t(i, d):
419  W.n_mod_lt(U32.to_nat(i), Nat.pow(2n, d), B.pow_pos(d))
420
421law 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
427def slot_small_t(i, d, h):
428  W.n_mod_small(U32.to_nat(i), Nat.pow(2n, d), h)
429
430law 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
436def 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
445law 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
453def 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
458law 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
468def 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
478law 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
489def 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
499law 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
510def 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
520law 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
531def 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).
548def 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
560law 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
569def 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
595def 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
600law 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
607def 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
619def 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
626law 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
639def 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)