1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../lib/u32.bend as U
5	import ../../lib/list.bend as LL
6	import ../../lib/array.bend as AR
7	import ../../../spec/lib/common.bend as SC
8	import ../../../src/containers/balanced_search_tree.bend as M
9	import ../dynamic_array/state.bend as DAS
10	import ./bk.bend as BK
11	import ./nsr.bend as NR
12	
13	# One field of the TreeMap's node store: the field list of a node list
14	# (length, reads, updates, appends, dropping the last) and the field's block
15	# under Array.get / Array.set / doubling, for every node list of length at
16	# most the capacity 2^d, d <= l <= 31.
17	
18	
19	# Some{x} gives x
20	def unsome(~K: Data, m: Maybe<&2, M.Node<K>>, +dv: M.Node<K>) -> M.Node<K>:
21	  match m:
22	    case None{}:
23	      dv
24	    case Some{x}:
25	      x
26	
27	def mb(~K: Data, m: Maybe<&2, M.Node<K>>) -> Bool:
28	  match m:
29	    case None{}:
30	      False{}
31	    case Some{x}:
32	      True{}
33	
34	def unsomeA(-A: Data, m: Maybe<&2, A>, +dv: A) -> A:
35	  match m:
36	    case None{}:
37	      dv
38	    case Some{x}:
39	      x
40	
41	# updating a slot with the value it holds changes nothing
42	def upd_same(-A: Data, +ys: List<&2, A>, +i: Nat, +z: A, +h: {SC.nth(A, ys, i) == Some{z} : Maybe<&2, A>}) -> {SC.update(A, ys, i, z) == ys : List<&2, A>}:
43	  match ys i:
44	    case Nil{} _:
45	      {==}
46	    case Con{+x, r} 0n:
47	      Equal.cong(Maybe<&2, A>, List<&2, A>, w => Con{unsomeA(A, w, x), r}, Some{z}, Some{x}, Equal.sym(Maybe<&2, A>, Some{x}, Some{z}, h))
48	    case Con{+x, +r} 1n+q:
49	      LL.cons_cong(A, x, SC.update(A, r, q, z), r, upd_same(A, r, q, z, h))
50	
51	def tags_len(~K: Data, +xs: List<&2, M.Node<K>>) -> {SC.length(Nat, NR.tags(~K, xs)) == SC.length(M.Node<K>, xs) : Nat}:
52	  match xs:
53	    case Nil{}:
54	      {==}
55	    case Con{x, +r}:
56	      N.succ_cong(SC.length(Nat, NR.tags(~K, r)), SC.length(M.Node<K>, r), tags_len(~K, r))
57	
58	def tags_nth(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>, +h: {SC.nth(M.Node<K>, xs, i) == Some{y} : Maybe<&2, M.Node<K>>}) -> {SC.nth(Nat, NR.tags(~K, xs), i) == Some{M.ntag(~K, y)} : Maybe<&2, Nat>}:
59	  match xs i:
60	    case Nil{} _:
61	      Empty.absurd({SC.nth(Nat, Nil{}, i) == Some{M.ntag(~K, y)} : Maybe<&2, Nat>}, L.false_true(Equal.cong(Maybe<&2, M.Node<K>>, Bool, z => mb(~K, z), None{}, Some{y}, h)))
62	    case Con{+x, r} 0n:
63	      Equal.cong(Maybe<&2, M.Node<K>>, Maybe<&2, Nat>, z => Some{M.ntag(~K, unsome(~K, z, x))}, Some{x}, Some{y}, h)
64	    case Con{x, +r} 1n+q:
65	      tags_nth(~K, r, q, y, h)
66	
67	def tags_upd(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>) -> {SC.update(Nat, NR.tags(~K, xs), i, M.ntag(~K, y)) == NR.tags(~K, SC.update(M.Node<K>, xs, i, y)) : List<&2, Nat>}:
68	  match xs i:
69	    case Nil{} _:
70	      {==}
71	    case Con{x, r} 0n:
72	      {==}
73	    case Con{+x, +r} 1n+q:
74	      LL.cons_cong(Nat, M.ntag(~K, x), SC.update(Nat, NR.tags(~K, r), q, M.ntag(~K, y)), NR.tags(~K, SC.update(M.Node<K>, r, q, y)), tags_upd(~K, r, q, y))
75	
76	def tags_snoc(~K: Data, +xs: List<&2, M.Node<K>>, +y: M.Node<K>) -> {SC.snoc(Nat, NR.tags(~K, xs), M.ntag(~K, y)) == NR.tags(~K, SC.snoc(M.Node<K>, xs, y)) : List<&2, Nat>}:
77	  match xs:
78	    case Nil{}:
79	      {==}
80	    case Con{+x, +r}:
81	      LL.cons_cong(Nat, M.ntag(~K, x), SC.snoc(Nat, NR.tags(~K, r), M.ntag(~K, y)), NR.tags(~K, SC.snoc(M.Node<K>, r, y)), tags_snoc(~K, r, y))
82	
83	def tags_init(~K: Data, +xs: List<&2, M.Node<K>>) -> {SC.init(Nat, NR.tags(~K, xs)) == NR.tags(~K, SC.init(M.Node<K>, xs)) : List<&2, Nat>}:
84	  match xs:
85	    case Nil{}:
86	      {==}
87	    case Con{x, Nil{}}:
88	      {==}
89	    case Con{+x, Con{+y, +t}}:
90	      LL.cons_cong(Nat, M.ntag(~K, x), SC.init(Nat, NR.tags(~K, Con{y, t})), NR.tags(~K, SC.init(M.Node<K>, Con{y, t})), tags_init(~K, Con{y, t}))
91	
92	# the field block: a slot below the length reads the field
93	def tag_get(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +y: M.Node<K>, +hy: {SC.nth(M.Node<K>, xs, i) == Some{y} : Maybe<&2, M.Node<K>>}) -> {Array.get(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(i)) == (AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), M.ntag(~K, y)) : Array<Nat> & Nat}:
94	  +fl = NR.tags(~K, xs)
95	  +t = BK.bk(Nat, d, fl, 0n)
96	  +hlen = tags_len(~K, xs)
97	  +hi = LL.nth_lt_length(M.Node<K>, xs, i, y, hy)
98	  +hip = N.lt_le_trans(i, SC.length(M.Node<K>, xs), SC.pow2(d), hi, hc)
99	  +eu = U.to_nat_from_nat(i, d, DAS.le32(d, l, hd, hl), hip)
100	  +hiF = L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hi)
101	  +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hc)
102	  +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), i), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), Some{M.ntag(~K, y)}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, i), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), SC.nth(Nat, fl, i), Some{M.ntag(~K, y)}, BK.fill_nth(Nat, SC.pow2(d), fl, 0n, i, hiF, hcF), tags_nth(~K, xs, i, y, hy)))
103	  +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{M.ntag(~K, y)} : Maybe<&2, Nat>}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hx0)
104	  +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hip)
105	  AR.get(Nat, d, t, U32.from_nat(i), M.ntag(~K, y), DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))
106	
107	# a slot below the length written with a node's field
108	def tag_set(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +y0: M.Node<K>, +hy0: {SC.nth(M.Node<K>, xs, i) == Some{y0} : Maybe<&2, M.Node<K>>}, +y: M.Node<K>) -> {Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(i), M.ntag(~K, y)) == AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, y)), 0n)) : Array<Nat>}:
109	  +fl = NR.tags(~K, xs)
110	  +t = BK.bk(Nat, d, fl, 0n)
111	  +hlen = tags_len(~K, xs)
112	  +hi = LL.nth_lt_length(M.Node<K>, xs, i, y0, hy0)
113	  +hip = N.lt_le_trans(i, SC.length(M.Node<K>, xs), SC.pow2(d), hi, hc)
114	  +eu = U.to_nat_from_nat(i, d, DAS.le32(d, l, hd, hl), hip)
115	  +hiF = L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hi)
116	  +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hc)
117	  +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), i), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), Some{M.ntag(~K, y0)}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, i), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), SC.nth(Nat, fl, i), Some{M.ntag(~K, y0)}, BK.fill_nth(Nat, SC.pow2(d), fl, 0n, i, hiF, hcF), tags_nth(~K, xs, i, y0, hy0)))
118	  +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{M.ntag(~K, y0)} : Maybe<&2, Nat>}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hx0)
119	  +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hip)
120	  %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, t), U32.from_nat(i), M.ntag(~K, y)), AR.thaw(Nat, AR.upd(Nat, d, t, U32.to_nat(U32.from_nat(i)), M.ntag(~K, y))), AR.set(Nat, d, t, U32.from_nat(i), M.ntag(~K, y), M.ntag(~K, y0), DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))) : {_ == AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, y)), 0n)) : Array<Nat>}
121	  %Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu) : {AR.thaw(Nat, AR.upd(Nat, d, t, _, M.ntag(~K, y))) == AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, y)), 0n)) : Array<Nat>}
122	  Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.upd(Nat, d, t, i, M.ntag(~K, y)), BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, y)), 0n), Equal.trans(AR.Tree<Nat>, AR.upd(Nat, d, t, i, M.ntag(~K, y)), BK.bk(Nat, d, SC.update(Nat, fl, i, M.ntag(~K, y)), 0n), BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, y)), 0n), BK.bk_set(Nat, d, fl, 0n, i, M.ntag(~K, y), hiF, hcF), Equal.cong(List<&2, Nat>, AR.Tree<Nat>, z => BK.bk(Nat, d, z, 0n), SC.update(Nat, fl, i, M.ntag(~K, y)), NR.tags(~K, SC.update(M.Node<K>, xs, i, y)), tags_upd(~K, xs, i, y))))
123	
124	# the slot at the length (inside the capacity) written: an append
125	def tag_push(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +y: M.Node<K>, +hn: {Nat.is_lt(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}) -> {Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(SC.length(M.Node<K>, xs)), M.ntag(~K, y)) == AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}:
126	  +fl = NR.tags(~K, xs)
127	  +t = BK.bk(Nat, d, fl, 0n)
128	  +n = SC.length(M.Node<K>, xs)
129	  +hlen = tags_len(~K, xs)
130	  +eu = U.to_nat_from_nat(n, d, DAS.le32(d, l, hd, hl), hn)
131	  +hnF = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, n, SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), n, hlen), hn)
132	  +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), SC.length(Nat, fl)), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), SC.length(Nat, fl)), Some{0n}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, SC.length(Nat, fl)), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), BK.fill_at_len(Nat, SC.pow2(d), fl, 0n, hnF))
133	  +hx1 = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{0n} : Maybe<&2, Nat>}, SC.length(Nat, fl), n, hlen, hx0)
134	  +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{0n} : Maybe<&2, Nat>}, n, U32.to_nat(U32.from_nat(n)), Equal.sym(Nat, U32.to_nat(U32.from_nat(n)), n, eu), hx1)
135	  +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, n, U32.to_nat(U32.from_nat(n)), Equal.sym(Nat, U32.to_nat(U32.from_nat(n)), n, eu), hn)
136	  %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, t), U32.from_nat(n), M.ntag(~K, y)), AR.thaw(Nat, AR.upd(Nat, d, t, U32.to_nat(U32.from_nat(n)), M.ntag(~K, y))), AR.set(Nat, d, t, U32.from_nat(n), M.ntag(~K, y), 0n, DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))) : {_ == AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}
137	  %Equal.sym(Nat, U32.to_nat(U32.from_nat(n)), n, eu) : {AR.thaw(Nat, AR.upd(Nat, d, t, _, M.ntag(~K, y))) == AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}
138	  %hlen : {AR.thaw(Nat, AR.upd(Nat, d, t, _, M.ntag(~K, y))) == AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}
139	  Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.upd(Nat, d, t, SC.length(Nat, fl), M.ntag(~K, y)), BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node<K>, xs, y)), 0n), Equal.trans(AR.Tree<Nat>, AR.upd(Nat, d, t, SC.length(Nat, fl), M.ntag(~K, y)), BK.bk(Nat, d, SC.snoc(Nat, fl, M.ntag(~K, y)), 0n), BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node<K>, xs, y)), 0n), BK.bk_push(Nat, d, fl, 0n, M.ntag(~K, y), hnF), Equal.cong(List<&2, Nat>, AR.Tree<Nat>, z => BK.bk(Nat, d, z, 0n), SC.snoc(Nat, fl, M.ntag(~K, y)), NR.tags(~K, SC.snoc(M.Node<K>, xs, y)), tags_snoc(~K, xs, y))))
140	
141	# the block doubled with a default half
142	def tag_grow(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}) -> {ANode{AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), Array.new(Nat, d, 0n)} == AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.tags(~K, xs), 0n)) : Array<Nat>}:
143	  +fl = NR.tags(~K, xs)
144	  +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), tags_len(~K, xs)), hc)
145	  %Equal.sym(Array<Nat>, Array.new(Nat, d, 0n), AR.thaw(Nat, AR.trep(Nat, d, 0n)), AR.new(Nat, d, 0n)) : {ANode{AR.thaw(Nat, BK.bk(Nat, d, fl, 0n)), _} == AR.thaw(Nat, BK.bk(Nat, 1n+d, fl, 0n)) : Array<Nat>}
146	  Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.TNode{BK.bk(Nat, d, fl, 0n), AR.trep(Nat, d, 0n)}, BK.bk(Nat, 1n+d, fl, 0n), BK.bk_grow(Nat, d, fl, 0n, hcF))
147	
148	# the last slot reset to the encoding of Free{0}: a pop
149	def tag_drop(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +m: Nat, +hm: {SC.length(M.Node<K>, xs) == 1n+m : Nat}, +y0: M.Node<K>, +hy0: {SC.nth(M.Node<K>, xs, m) == Some{y0} : Maybe<&2, M.Node<K>>}) -> {Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(m), M.ntag(~K, M.Free{0n})) == AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.init(M.Node<K>, xs)), 0n)) : Array<Nat>}:
150	  +fl = NR.tags(~K, xs)
151	  +t = BK.bk(Nat, d, fl, 0n)
152	  +hlen = tags_len(~K, xs)
153	  +hi = LL.nth_lt_length(M.Node<K>, xs, m, y0, hy0)
154	  +hip = N.lt_le_trans(m, SC.length(M.Node<K>, xs), SC.pow2(d), hi, hc)
155	  +eu = U.to_nat_from_nat(m, d, DAS.le32(d, l, hd, hl), hip)
156	  +hiF = L.subst(Nat, z => {Nat.is_lt(m, z) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hi)
157	  +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hc)
158	  +hmF = Equal.trans(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), 1n+m, hlen, hm)
159	  +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), m), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), m), Some{M.ntag(~K, y0)}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, m), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), m), SC.nth(Nat, fl, m), Some{M.ntag(~K, y0)}, BK.fill_nth(Nat, SC.pow2(d), fl, 0n, m, hiF, hcF), tags_nth(~K, xs, m, y0, hy0)))
160	  +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{M.ntag(~K, y0)} : Maybe<&2, Nat>}, m, U32.to_nat(U32.from_nat(m)), Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, eu), hx0)
161	  +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, m, U32.to_nat(U32.from_nat(m)), Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, eu), hip)
162	  %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, t), U32.from_nat(m), 0n), AR.thaw(Nat, AR.upd(Nat, d, t, U32.to_nat(U32.from_nat(m)), 0n)), AR.set(Nat, d, t, U32.from_nat(m), 0n, M.ntag(~K, y0), DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))) : {_ == AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.init(M.Node<K>, xs)), 0n)) : Array<Nat>}
163	  %Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, eu) : {AR.thaw(Nat, AR.upd(Nat, d, t, _, 0n)) == AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.init(M.Node<K>, xs)), 0n)) : Array<Nat>}
164	  Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.upd(Nat, d, t, m, 0n), BK.bk(Nat, d, NR.tags(~K, SC.init(M.Node<K>, xs)), 0n), Equal.trans(AR.Tree<Nat>, AR.upd(Nat, d, t, m, 0n), BK.bk(Nat, d, SC.init(Nat, fl), 0n), BK.bk(Nat, d, NR.tags(~K, SC.init(M.Node<K>, xs)), 0n), BK.bk_pop(Nat, d, fl, 0n, m, hmF, hcF), Equal.cong(List<&2, Nat>, AR.Tree<Nat>, z => BK.bk(Nat, d, z, 0n), SC.init(Nat, fl), NR.tags(~K, SC.init(M.Node<K>, xs)), tags_init(~K, xs))))
165	
166	# updating a node that keeps this field leaves the field list
167	def tags_keep(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>, +x: M.Node<K>, +hy: {SC.nth(M.Node<K>, xs, i) == Some{y} : Maybe<&2, M.Node<K>>}, +he: {M.ntag(~K, x) == M.ntag(~K, y) : Nat}) -> {NR.tags(~K, SC.update(M.Node<K>, xs, i, x)) == NR.tags(~K, xs) : List<&2, Nat>}:
168	  %tags_upd(~K, xs, i, x) : {_ == NR.tags(~K, xs) : List<&2, Nat>}
169	  %Equal.sym(Nat, M.ntag(~K, x), M.ntag(~K, y), he) : {SC.update(Nat, NR.tags(~K, xs), i, _) == NR.tags(~K, xs) : List<&2, Nat>}
170	  upd_same(Nat, NR.tags(~K, xs), i, M.ntag(~K, y), tags_nth(~K, xs, i, y, hy))
171	
172	def lefts_len(~K: Data, +xs: List<&2, M.Node<K>>) -> {SC.length(Nat, NR.lefts(~K, xs)) == SC.length(M.Node<K>, xs) : Nat}:
173	  match xs:
174	    case Nil{}:
175	      {==}
176	    case Con{x, +r}:
177	      N.succ_cong(SC.length(Nat, NR.lefts(~K, r)), SC.length(M.Node<K>, r), lefts_len(~K, r))
178	
179	def lefts_nth(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>, +h: {SC.nth(M.Node<K>, xs, i) == Some{y} : Maybe<&2, M.Node<K>>}) -> {SC.nth(Nat, NR.lefts(~K, xs), i) == Some{M.nleft(~K, y)} : Maybe<&2, Nat>}:
180	  match xs i:
181	    case Nil{} _:
182	      Empty.absurd({SC.nth(Nat, Nil{}, i) == Some{M.nleft(~K, y)} : Maybe<&2, Nat>}, L.false_true(Equal.cong(Maybe<&2, M.Node<K>>, Bool, z => mb(~K, z), None{}, Some{y}, h)))
183	    case Con{+x, r} 0n:
184	      Equal.cong(Maybe<&2, M.Node<K>>, Maybe<&2, Nat>, z => Some{M.nleft(~K, unsome(~K, z, x))}, Some{x}, Some{y}, h)
185	    case Con{x, +r} 1n+q:
186	      lefts_nth(~K, r, q, y, h)
187	
188	def lefts_upd(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>) -> {SC.update(Nat, NR.lefts(~K, xs), i, M.nleft(~K, y)) == NR.lefts(~K, SC.update(M.Node<K>, xs, i, y)) : List<&2, Nat>}:
189	  match xs i:
190	    case Nil{} _:
191	      {==}
192	    case Con{x, r} 0n:
193	      {==}
194	    case Con{+x, +r} 1n+q:
195	      LL.cons_cong(Nat, M.nleft(~K, x), SC.update(Nat, NR.lefts(~K, r), q, M.nleft(~K, y)), NR.lefts(~K, SC.update(M.Node<K>, r, q, y)), lefts_upd(~K, r, q, y))
196	
197	def lefts_snoc(~K: Data, +xs: List<&2, M.Node<K>>, +y: M.Node<K>) -> {SC.snoc(Nat, NR.lefts(~K, xs), M.nleft(~K, y)) == NR.lefts(~K, SC.snoc(M.Node<K>, xs, y)) : List<&2, Nat>}:
198	  match xs:
199	    case Nil{}:
200	      {==}
201	    case Con{+x, +r}:
202	      LL.cons_cong(Nat, M.nleft(~K, x), SC.snoc(Nat, NR.lefts(~K, r), M.nleft(~K, y)), NR.lefts(~K, SC.snoc(M.Node<K>, r, y)), lefts_snoc(~K, r, y))
203	
204	def lefts_init(~K: Data, +xs: List<&2, M.Node<K>>) -> {SC.init(Nat, NR.lefts(~K, xs)) == NR.lefts(~K, SC.init(M.Node<K>, xs)) : List<&2, Nat>}:
205	  match xs:
206	    case Nil{}:
207	      {==}
208	    case Con{x, Nil{}}:
209	      {==}
210	    case Con{+x, Con{+y, +t}}:
211	      LL.cons_cong(Nat, M.nleft(~K, x), SC.init(Nat, NR.lefts(~K, Con{y, t})), NR.lefts(~K, SC.init(M.Node<K>, Con{y, t})), lefts_init(~K, Con{y, t}))
212	
213	# the field block: a slot below the length reads the field
214	def left_get(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +y: M.Node<K>, +hy: {SC.nth(M.Node<K>, xs, i) == Some{y} : Maybe<&2, M.Node<K>>}) -> {Array.get(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), U32.from_nat(i)) == (AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), M.nleft(~K, y)) : Array<Nat> & Nat}:
215	  +fl = NR.lefts(~K, xs)
216	  +t = BK.bk(Nat, d, fl, 0n)
217	  +hlen = lefts_len(~K, xs)
218	  +hi = LL.nth_lt_length(M.Node<K>, xs, i, y, hy)
219	  +hip = N.lt_le_trans(i, SC.length(M.Node<K>, xs), SC.pow2(d), hi, hc)
220	  +eu = U.to_nat_from_nat(i, d, DAS.le32(d, l, hd, hl), hip)
221	  +hiF = L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hi)
222	  +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hc)
223	  +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), i), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), Some{M.nleft(~K, y)}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, i), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), SC.nth(Nat, fl, i), Some{M.nleft(~K, y)}, BK.fill_nth(Nat, SC.pow2(d), fl, 0n, i, hiF, hcF), lefts_nth(~K, xs, i, y, hy)))
224	  +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{M.nleft(~K, y)} : Maybe<&2, Nat>}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hx0)
225	  +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hip)
226	  AR.get(Nat, d, t, U32.from_nat(i), M.nleft(~K, y), DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))
227	
228	# a slot below the length written with a node's field
229	def left_set(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +y0: M.Node<K>, +hy0: {SC.nth(M.Node<K>, xs, i) == Some{y0} : Maybe<&2, M.Node<K>>}, +y: M.Node<K>) -> {Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), U32.from_nat(i), M.nleft(~K, y)) == AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, y)), 0n)) : Array<Nat>}:
230	  +fl = NR.lefts(~K, xs)
231	  +t = BK.bk(Nat, d, fl, 0n)
232	  +hlen = lefts_len(~K, xs)
233	  +hi = LL.nth_lt_length(M.Node<K>, xs, i, y0, hy0)
234	  +hip = N.lt_le_trans(i, SC.length(M.Node<K>, xs), SC.pow2(d), hi, hc)
235	  +eu = U.to_nat_from_nat(i, d, DAS.le32(d, l, hd, hl), hip)
236	  +hiF = L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hi)
237	  +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hc)
238	  +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), i), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), Some{M.nleft(~K, y0)}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, i), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), SC.nth(Nat, fl, i), Some{M.nleft(~K, y0)}, BK.fill_nth(Nat, SC.pow2(d), fl, 0n, i, hiF, hcF), lefts_nth(~K, xs, i, y0, hy0)))
239	  +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{M.nleft(~K, y0)} : Maybe<&2, Nat>}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hx0)
240	  +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hip)
241	  %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, t), U32.from_nat(i), M.nleft(~K, y)), AR.thaw(Nat, AR.upd(Nat, d, t, U32.to_nat(U32.from_nat(i)), M.nleft(~K, y))), AR.set(Nat, d, t, U32.from_nat(i), M.nleft(~K, y), M.nleft(~K, y0), DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))) : {_ == AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, y)), 0n)) : Array<Nat>}
242	  %Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu) : {AR.thaw(Nat, AR.upd(Nat, d, t, _, M.nleft(~K, y))) == AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, y)), 0n)) : Array<Nat>}
243	  Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.upd(Nat, d, t, i, M.nleft(~K, y)), BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, y)), 0n), Equal.trans(AR.Tree<Nat>, AR.upd(Nat, d, t, i, M.nleft(~K, y)), BK.bk(Nat, d, SC.update(Nat, fl, i, M.nleft(~K, y)), 0n), BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, y)), 0n), BK.bk_set(Nat, d, fl, 0n, i, M.nleft(~K, y), hiF, hcF), Equal.cong(List<&2, Nat>, AR.Tree<Nat>, z => BK.bk(Nat, d, z, 0n), SC.update(Nat, fl, i, M.nleft(~K, y)), NR.lefts(~K, SC.update(M.Node<K>, xs, i, y)), lefts_upd(~K, xs, i, y))))
244	
245	# the slot at the length (inside the capacity) written: an append
246	def left_push(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +y: M.Node<K>, +hn: {Nat.is_lt(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}) -> {Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), U32.from_nat(SC.length(M.Node<K>, xs)), M.nleft(~K, y)) == AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}:
247	  +fl = NR.lefts(~K, xs)
248	  +t = BK.bk(Nat, d, fl, 0n)
249	  +n = SC.length(M.Node<K>, xs)
250	  +hlen = lefts_len(~K, xs)
251	  +eu = U.to_nat_from_nat(n, d, DAS.le32(d, l, hd, hl), hn)
252	  +hnF = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, n, SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), n, hlen), hn)
253	  +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), SC.length(Nat, fl)), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), SC.length(Nat, fl)), Some{0n}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, SC.length(Nat, fl)), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), BK.fill_at_len(Nat, SC.pow2(d), fl, 0n, hnF))
254	  +hx1 = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{0n} : Maybe<&2, Nat>}, SC.length(Nat, fl), n, hlen, hx0)
255	  +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{0n} : Maybe<&2, Nat>}, n, U32.to_nat(U32.from_nat(n)), Equal.sym(Nat, U32.to_nat(U32.from_nat(n)), n, eu), hx1)
256	  +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, n, U32.to_nat(U32.from_nat(n)), Equal.sym(Nat, U32.to_nat(U32.from_nat(n)), n, eu), hn)
257	  %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, t), U32.from_nat(n), M.nleft(~K, y)), AR.thaw(Nat, AR.upd(Nat, d, t, U32.to_nat(U32.from_nat(n)), M.nleft(~K, y))), AR.set(Nat, d, t, U32.from_nat(n), M.nleft(~K, y), 0n, DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))) : {_ == AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}
258	  %Equal.sym(Nat, U32.to_nat(U32.from_nat(n)), n, eu) : {AR.thaw(Nat, AR.upd(Nat, d, t, _, M.nleft(~K, y))) == AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}
259	  %hlen : {AR.thaw(Nat, AR.upd(Nat, d, t, _, M.nleft(~K, y))) == AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}
260	  Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.upd(Nat, d, t, SC.length(Nat, fl), M.nleft(~K, y)), BK.bk(Nat, d, NR.lefts(~K, SC.snoc(M.Node<K>, xs, y)), 0n), Equal.trans(AR.Tree<Nat>, AR.upd(Nat, d, t, SC.length(Nat, fl), M.nleft(~K, y)), BK.bk(Nat, d, SC.snoc(Nat, fl, M.nleft(~K, y)), 0n), BK.bk(Nat, d, NR.lefts(~K, SC.snoc(M.Node<K>, xs, y)), 0n), BK.bk_push(Nat, d, fl, 0n, M.nleft(~K, y), hnF), Equal.cong(List<&2, Nat>, AR.Tree<Nat>, z => BK.bk(Nat, d, z, 0n), SC.snoc(Nat, fl, M.nleft(~K, y)), NR.lefts(~K, SC.snoc(M.Node<K>, xs, y)), lefts_snoc(~K, xs, y))))
261	
262	# the block doubled with a default half
263	def left_grow(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}) -> {ANode{AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), Array.new(Nat, d, 0n)} == AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.lefts(~K, xs), 0n)) : Array<Nat>}:
264	  +fl = NR.lefts(~K, xs)
265	  +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), lefts_len(~K, xs)), hc)
266	  %Equal.sym(Array<Nat>, Array.new(Nat, d, 0n), AR.thaw(Nat, AR.trep(Nat, d, 0n)), AR.new(Nat, d, 0n)) : {ANode{AR.thaw(Nat, BK.bk(Nat, d, fl, 0n)), _} == AR.thaw(Nat, BK.bk(Nat, 1n+d, fl, 0n)) : Array<Nat>}
267	  Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.TNode{BK.bk(Nat, d, fl, 0n), AR.trep(Nat, d, 0n)}, BK.bk(Nat, 1n+d, fl, 0n), BK.bk_grow(Nat, d, fl, 0n, hcF))
268	
269	# the last slot reset to the encoding of Free{0}: a pop
270	def left_drop(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +m: Nat, +hm: {SC.length(M.Node<K>, xs) == 1n+m : Nat}, +y0: M.Node<K>, +hy0: {SC.nth(M.Node<K>, xs, m) == Some{y0} : Maybe<&2, M.Node<K>>}) -> {Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), U32.from_nat(m), M.nleft(~K, M.Free{0n})) == AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.init(M.Node<K>, xs)), 0n)) : Array<Nat>}:
271	  +fl = NR.lefts(~K, xs)
272	  +t = BK.bk(Nat, d, fl, 0n)
273	  +hlen = lefts_len(~K, xs)
274	  +hi = LL.nth_lt_length(M.Node<K>, xs, m, y0, hy0)
275	  +hip = N.lt_le_trans(m, SC.length(M.Node<K>, xs), SC.pow2(d), hi, hc)
276	  +eu = U.to_nat_from_nat(m, d, DAS.le32(d, l, hd, hl), hip)
277	  +hiF = L.subst(Nat, z => {Nat.is_lt(m, z) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hi)
278	  +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hc)
279	  +hmF = Equal.trans(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), 1n+m, hlen, hm)
280	  +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), m), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), m), Some{M.nleft(~K, y0)}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, m), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), m), SC.nth(Nat, fl, m), Some{M.nleft(~K, y0)}, BK.fill_nth(Nat, SC.pow2(d), fl, 0n, m, hiF, hcF), lefts_nth(~K, xs, m, y0, hy0)))
281	  +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{M.nleft(~K, y0)} : Maybe<&2, Nat>}, m, U32.to_nat(U32.from_nat(m)), Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, eu), hx0)
282	  +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, m, U32.to_nat(U32.from_nat(m)), Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, eu), hip)
283	  %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, t), U32.from_nat(m), 0n), AR.thaw(Nat, AR.upd(Nat, d, t, U32.to_nat(U32.from_nat(m)), 0n)), AR.set(Nat, d, t, U32.from_nat(m), 0n, M.nleft(~K, y0), DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))) : {_ == AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.init(M.Node<K>, xs)), 0n)) : Array<Nat>}
284	  %Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, eu) : {AR.thaw(Nat, AR.upd(Nat, d, t, _, 0n)) == AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.init(M.Node<K>, xs)), 0n)) : Array<Nat>}
285	  Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.upd(Nat, d, t, m, 0n), BK.bk(Nat, d, NR.lefts(~K, SC.init(M.Node<K>, xs)), 0n), Equal.trans(AR.Tree<Nat>, AR.upd(Nat, d, t, m, 0n), BK.bk(Nat, d, SC.init(Nat, fl), 0n), BK.bk(Nat, d, NR.lefts(~K, SC.init(M.Node<K>, xs)), 0n), BK.bk_pop(Nat, d, fl, 0n, m, hmF, hcF), Equal.cong(List<&2, Nat>, AR.Tree<Nat>, z => BK.bk(Nat, d, z, 0n), SC.init(Nat, fl), NR.lefts(~K, SC.init(M.Node<K>, xs)), lefts_init(~K, xs))))
286	
287	# updating a node that keeps this field leaves the field list
288	def lefts_keep(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>, +x: M.Node<K>, +hy: {SC.nth(M.Node<K>, xs, i) == Some{y} : Maybe<&2, M.Node<K>>}, +he: {M.nleft(~K, x) == M.nleft(~K, y) : Nat}) -> {NR.lefts(~K, SC.update(M.Node<K>, xs, i, x)) == NR.lefts(~K, xs) : List<&2, Nat>}:
289	  %lefts_upd(~K, xs, i, x) : {_ == NR.lefts(~K, xs) : List<&2, Nat>}
290	  %Equal.sym(Nat, M.nleft(~K, x), M.nleft(~K, y), he) : {SC.update(Nat, NR.lefts(~K, xs), i, _) == NR.lefts(~K, xs) : List<&2, Nat>}
291	  upd_same(Nat, NR.lefts(~K, xs), i, M.nleft(~K, y), lefts_nth(~K, xs, i, y, hy))
292	
293	def rights_len(~K: Data, +xs: List<&2, M.Node<K>>) -> {SC.length(Nat, NR.rights(~K, xs)) == SC.length(M.Node<K>, xs) : Nat}:
294	  match xs:
295	    case Nil{}:
296	      {==}
297	    case Con{x, +r}:
298	      N.succ_cong(SC.length(Nat, NR.rights(~K, r)), SC.length(M.Node<K>, r), rights_len(~K, r))
299	
300	def rights_nth(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>, +h: {SC.nth(M.Node<K>, xs, i) == Some{y} : Maybe<&2, M.Node<K>>}) -> {SC.nth(Nat, NR.rights(~K, xs), i) == Some{M.nright(~K, y)} : Maybe<&2, Nat>}:
301	  match xs i:
302	    case Nil{} _:
303	      Empty.absurd({SC.nth(Nat, Nil{}, i) == Some{M.nright(~K, y)} : Maybe<&2, Nat>}, L.false_true(Equal.cong(Maybe<&2, M.Node<K>>, Bool, z => mb(~K, z), None{}, Some{y}, h)))
304	    case Con{+x, r} 0n:
305	      Equal.cong(Maybe<&2, M.Node<K>>, Maybe<&2, Nat>, z => Some{M.nright(~K, unsome(~K, z, x))}, Some{x}, Some{y}, h)
306	    case Con{x, +r} 1n+q:
307	      rights_nth(~K, r, q, y, h)
308	
309	def rights_upd(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>) -> {SC.update(Nat, NR.rights(~K, xs), i, M.nright(~K, y)) == NR.rights(~K, SC.update(M.Node<K>, xs, i, y)) : List<&2, Nat>}:
310	  match xs i:
311	    case Nil{} _:
312	      {==}
313	    case Con{x, r} 0n:
314	      {==}
315	    case Con{+x, +r} 1n+q:
316	      LL.cons_cong(Nat, M.nright(~K, x), SC.update(Nat, NR.rights(~K, r), q, M.nright(~K, y)), NR.rights(~K, SC.update(M.Node<K>, r, q, y)), rights_upd(~K, r, q, y))
317	
318	def rights_snoc(~K: Data, +xs: List<&2, M.Node<K>>, +y: M.Node<K>) -> {SC.snoc(Nat, NR.rights(~K, xs), M.nright(~K, y)) == NR.rights(~K, SC.snoc(M.Node<K>, xs, y)) : List<&2, Nat>}:
319	  match xs:
320	    case Nil{}:
321	      {==}
322	    case Con{+x, +r}:
323	      LL.cons_cong(Nat, M.nright(~K, x), SC.snoc(Nat, NR.rights(~K, r), M.nright(~K, y)), NR.rights(~K, SC.snoc(M.Node<K>, r, y)), rights_snoc(~K, r, y))
324	
325	def rights_init(~K: Data, +xs: List<&2, M.Node<K>>) -> {SC.init(Nat, NR.rights(~K, xs)) == NR.rights(~K, SC.init(M.Node<K>, xs)) : List<&2, Nat>}:
326	  match xs:
327	    case Nil{}:
328	      {==}
329	    case Con{x, Nil{}}:
330	      {==}
331	    case Con{+x, Con{+y, +t}}:
332	      LL.cons_cong(Nat, M.nright(~K, x), SC.init(Nat, NR.rights(~K, Con{y, t})), NR.rights(~K, SC.init(M.Node<K>, Con{y, t})), rights_init(~K, Con{y, t}))
333	
334	# the field block: a slot below the length reads the field
335	def right_get(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +y: M.Node<K>, +hy: {SC.nth(M.Node<K>, xs, i) == Some{y} : Maybe<&2, M.Node<K>>}) -> {Array.get(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), U32.from_nat(i)) == (AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), M.nright(~K, y)) : Array<Nat> & Nat}:
336	  +fl = NR.rights(~K, xs)
337	  +t = BK.bk(Nat, d, fl, 0n)
338	  +hlen = rights_len(~K, xs)
339	  +hi = LL.nth_lt_length(M.Node<K>, xs, i, y, hy)
340	  +hip = N.lt_le_trans(i, SC.length(M.Node<K>, xs), SC.pow2(d), hi, hc)
341	  +eu = U.to_nat_from_nat(i, d, DAS.le32(d, l, hd, hl), hip)
342	  +hiF = L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hi)
343	  +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hc)
344	  +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), i), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), Some{M.nright(~K, y)}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, i), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), SC.nth(Nat, fl, i), Some{M.nright(~K, y)}, BK.fill_nth(Nat, SC.pow2(d), fl, 0n, i, hiF, hcF), rights_nth(~K, xs, i, y, hy)))
345	  +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{M.nright(~K, y)} : Maybe<&2, Nat>}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hx0)
346	  +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hip)
347	  AR.get(Nat, d, t, U32.from_nat(i), M.nright(~K, y), DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))
348	
349	# a slot below the length written with a node's field
350	def right_set(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +y0: M.Node<K>, +hy0: {SC.nth(M.Node<K>, xs, i) == Some{y0} : Maybe<&2, M.Node<K>>}, +y: M.Node<K>) -> {Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), U32.from_nat(i), M.nright(~K, y)) == AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, y)), 0n)) : Array<Nat>}:
351	  +fl = NR.rights(~K, xs)
352	  +t = BK.bk(Nat, d, fl, 0n)
353	  +hlen = rights_len(~K, xs)
354	  +hi = LL.nth_lt_length(M.Node<K>, xs, i, y0, hy0)
355	  +hip = N.lt_le_trans(i, SC.length(M.Node<K>, xs), SC.pow2(d), hi, hc)
356	  +eu = U.to_nat_from_nat(i, d, DAS.le32(d, l, hd, hl), hip)
357	  +hiF = L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hi)
358	  +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hc)
359	  +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), i), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), Some{M.nright(~K, y0)}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, i), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), SC.nth(Nat, fl, i), Some{M.nright(~K, y0)}, BK.fill_nth(Nat, SC.pow2(d), fl, 0n, i, hiF, hcF), rights_nth(~K, xs, i, y0, hy0)))
360	  +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{M.nright(~K, y0)} : Maybe<&2, Nat>}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hx0)
361	  +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hip)
362	  %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, t), U32.from_nat(i), M.nright(~K, y)), AR.thaw(Nat, AR.upd(Nat, d, t, U32.to_nat(U32.from_nat(i)), M.nright(~K, y))), AR.set(Nat, d, t, U32.from_nat(i), M.nright(~K, y), M.nright(~K, y0), DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))) : {_ == AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, y)), 0n)) : Array<Nat>}
363	  %Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu) : {AR.thaw(Nat, AR.upd(Nat, d, t, _, M.nright(~K, y))) == AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, y)), 0n)) : Array<Nat>}
364	  Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.upd(Nat, d, t, i, M.nright(~K, y)), BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, y)), 0n), Equal.trans(AR.Tree<Nat>, AR.upd(Nat, d, t, i, M.nright(~K, y)), BK.bk(Nat, d, SC.update(Nat, fl, i, M.nright(~K, y)), 0n), BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, y)), 0n), BK.bk_set(Nat, d, fl, 0n, i, M.nright(~K, y), hiF, hcF), Equal.cong(List<&2, Nat>, AR.Tree<Nat>, z => BK.bk(Nat, d, z, 0n), SC.update(Nat, fl, i, M.nright(~K, y)), NR.rights(~K, SC.update(M.Node<K>, xs, i, y)), rights_upd(~K, xs, i, y))))
365	
366	# the slot at the length (inside the capacity) written: an append
367	def right_push(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +y: M.Node<K>, +hn: {Nat.is_lt(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}) -> {Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), U32.from_nat(SC.length(M.Node<K>, xs)), M.nright(~K, y)) == AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}:
368	  +fl = NR.rights(~K, xs)
369	  +t = BK.bk(Nat, d, fl, 0n)
370	  +n = SC.length(M.Node<K>, xs)
371	  +hlen = rights_len(~K, xs)
372	  +eu = U.to_nat_from_nat(n, d, DAS.le32(d, l, hd, hl), hn)
373	  +hnF = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, n, SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), n, hlen), hn)
374	  +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), SC.length(Nat, fl)), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), SC.length(Nat, fl)), Some{0n}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, SC.length(Nat, fl)), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), BK.fill_at_len(Nat, SC.pow2(d), fl, 0n, hnF))
375	  +hx1 = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{0n} : Maybe<&2, Nat>}, SC.length(Nat, fl), n, hlen, hx0)
376	  +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{0n} : Maybe<&2, Nat>}, n, U32.to_nat(U32.from_nat(n)), Equal.sym(Nat, U32.to_nat(U32.from_nat(n)), n, eu), hx1)
377	  +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, n, U32.to_nat(U32.from_nat(n)), Equal.sym(Nat, U32.to_nat(U32.from_nat(n)), n, eu), hn)
378	  %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, t), U32.from_nat(n), M.nright(~K, y)), AR.thaw(Nat, AR.upd(Nat, d, t, U32.to_nat(U32.from_nat(n)), M.nright(~K, y))), AR.set(Nat, d, t, U32.from_nat(n), M.nright(~K, y), 0n, DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))) : {_ == AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}
379	  %Equal.sym(Nat, U32.to_nat(U32.from_nat(n)), n, eu) : {AR.thaw(Nat, AR.upd(Nat, d, t, _, M.nright(~K, y))) == AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}
380	  %hlen : {AR.thaw(Nat, AR.upd(Nat, d, t, _, M.nright(~K, y))) == AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}
381	  Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.upd(Nat, d, t, SC.length(Nat, fl), M.nright(~K, y)), BK.bk(Nat, d, NR.rights(~K, SC.snoc(M.Node<K>, xs, y)), 0n), Equal.trans(AR.Tree<Nat>, AR.upd(Nat, d, t, SC.length(Nat, fl), M.nright(~K, y)), BK.bk(Nat, d, SC.snoc(Nat, fl, M.nright(~K, y)), 0n), BK.bk(Nat, d, NR.rights(~K, SC.snoc(M.Node<K>, xs, y)), 0n), BK.bk_push(Nat, d, fl, 0n, M.nright(~K, y), hnF), Equal.cong(List<&2, Nat>, AR.Tree<Nat>, z => BK.bk(Nat, d, z, 0n), SC.snoc(Nat, fl, M.nright(~K, y)), NR.rights(~K, SC.snoc(M.Node<K>, xs, y)), rights_snoc(~K, xs, y))))
382	
383	# the block doubled with a default half
384	def right_grow(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}) -> {ANode{AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), Array.new(Nat, d, 0n)} == AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.rights(~K, xs), 0n)) : Array<Nat>}:
385	  +fl = NR.rights(~K, xs)
386	  +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), rights_len(~K, xs)), hc)
387	  %Equal.sym(Array<Nat>, Array.new(Nat, d, 0n), AR.thaw(Nat, AR.trep(Nat, d, 0n)), AR.new(Nat, d, 0n)) : {ANode{AR.thaw(Nat, BK.bk(Nat, d, fl, 0n)), _} == AR.thaw(Nat, BK.bk(Nat, 1n+d, fl, 0n)) : Array<Nat>}
388	  Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.TNode{BK.bk(Nat, d, fl, 0n), AR.trep(Nat, d, 0n)}, BK.bk(Nat, 1n+d, fl, 0n), BK.bk_grow(Nat, d, fl, 0n, hcF))
389	
390	# the last slot reset to the encoding of Free{0}: a pop
391	def right_drop(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +m: Nat, +hm: {SC.length(M.Node<K>, xs) == 1n+m : Nat}, +y0: M.Node<K>, +hy0: {SC.nth(M.Node<K>, xs, m) == Some{y0} : Maybe<&2, M.Node<K>>}) -> {Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), U32.from_nat(m), M.nright(~K, M.Free{0n})) == AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.init(M.Node<K>, xs)), 0n)) : Array<Nat>}:
392	  +fl = NR.rights(~K, xs)
393	  +t = BK.bk(Nat, d, fl, 0n)
394	  +hlen = rights_len(~K, xs)
395	  +hi = LL.nth_lt_length(M.Node<K>, xs, m, y0, hy0)
396	  +hip = N.lt_le_trans(m, SC.length(M.Node<K>, xs), SC.pow2(d), hi, hc)
397	  +eu = U.to_nat_from_nat(m, d, DAS.le32(d, l, hd, hl), hip)
398	  +hiF = L.subst(Nat, z => {Nat.is_lt(m, z) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hi)
399	  +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hc)
400	  +hmF = Equal.trans(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), 1n+m, hlen, hm)
401	  +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), m), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), m), Some{M.nright(~K, y0)}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, m), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), m), SC.nth(Nat, fl, m), Some{M.nright(~K, y0)}, BK.fill_nth(Nat, SC.pow2(d), fl, 0n, m, hiF, hcF), rights_nth(~K, xs, m, y0, hy0)))
402	  +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{M.nright(~K, y0)} : Maybe<&2, Nat>}, m, U32.to_nat(U32.from_nat(m)), Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, eu), hx0)
403	  +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, m, U32.to_nat(U32.from_nat(m)), Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, eu), hip)
404	  %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, t), U32.from_nat(m), 0n), AR.thaw(Nat, AR.upd(Nat, d, t, U32.to_nat(U32.from_nat(m)), 0n)), AR.set(Nat, d, t, U32.from_nat(m), 0n, M.nright(~K, y0), DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))) : {_ == AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.init(M.Node<K>, xs)), 0n)) : Array<Nat>}
405	  %Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, eu) : {AR.thaw(Nat, AR.upd(Nat, d, t, _, 0n)) == AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.init(M.Node<K>, xs)), 0n)) : Array<Nat>}
406	  Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.upd(Nat, d, t, m, 0n), BK.bk(Nat, d, NR.rights(~K, SC.init(M.Node<K>, xs)), 0n), Equal.trans(AR.Tree<Nat>, AR.upd(Nat, d, t, m, 0n), BK.bk(Nat, d, SC.init(Nat, fl), 0n), BK.bk(Nat, d, NR.rights(~K, SC.init(M.Node<K>, xs)), 0n), BK.bk_pop(Nat, d, fl, 0n, m, hmF, hcF), Equal.cong(List<&2, Nat>, AR.Tree<Nat>, z => BK.bk(Nat, d, z, 0n), SC.init(Nat, fl), NR.rights(~K, SC.init(M.Node<K>, xs)), rights_init(~K, xs))))
407	
408	# updating a node that keeps this field leaves the field list
409	def rights_keep(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>, +x: M.Node<K>, +hy: {SC.nth(M.Node<K>, xs, i) == Some{y} : Maybe<&2, M.Node<K>>}, +he: {M.nright(~K, x) == M.nright(~K, y) : Nat}) -> {NR.rights(~K, SC.update(M.Node<K>, xs, i, x)) == NR.rights(~K, xs) : List<&2, Nat>}:
410	  %rights_upd(~K, xs, i, x) : {_ == NR.rights(~K, xs) : List<&2, Nat>}
411	  %Equal.sym(Nat, M.nright(~K, x), M.nright(~K, y), he) : {SC.update(Nat, NR.rights(~K, xs), i, _) == NR.rights(~K, xs) : List<&2, Nat>}
412	  upd_same(Nat, NR.rights(~K, xs), i, M.nright(~K, y), rights_nth(~K, xs, i, y, hy))
413	
414	def parents_len(~K: Data, +xs: List<&2, M.Node<K>>) -> {SC.length(Nat, NR.parents(~K, xs)) == SC.length(M.Node<K>, xs) : Nat}:
415	  match xs:
416	    case Nil{}:
417	      {==}
418	    case Con{x, +r}:
419	      N.succ_cong(SC.length(Nat, NR.parents(~K, r)), SC.length(M.Node<K>, r), parents_len(~K, r))
420	
421	def parents_nth(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>, +h: {SC.nth(M.Node<K>, xs, i) == Some{y} : Maybe<&2, M.Node<K>>}) -> {SC.nth(Nat, NR.parents(~K, xs), i) == Some{M.nparent(~K, y)} : Maybe<&2, Nat>}:
422	  match xs i:
423	    case Nil{} _:
424	      Empty.absurd({SC.nth(Nat, Nil{}, i) == Some{M.nparent(~K, y)} : Maybe<&2, Nat>}, L.false_true(Equal.cong(Maybe<&2, M.Node<K>>, Bool, z => mb(~K, z), None{}, Some{y}, h)))
425	    case Con{+x, r} 0n:
426	      Equal.cong(Maybe<&2, M.Node<K>>, Maybe<&2, Nat>, z => Some{M.nparent(~K, unsome(~K, z, x))}, Some{x}, Some{y}, h)
427	    case Con{x, +r} 1n+q:
428	      parents_nth(~K, r, q, y, h)
429	
430	def parents_upd(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>) -> {SC.update(Nat, NR.parents(~K, xs), i, M.nparent(~K, y)) == NR.parents(~K, SC.update(M.Node<K>, xs, i, y)) : List<&2, Nat>}:
431	  match xs i:
432	    case Nil{} _:
433	      {==}
434	    case Con{x, r} 0n:
435	      {==}
436	    case Con{+x, +r} 1n+q:
437	      LL.cons_cong(Nat, M.nparent(~K, x), SC.update(Nat, NR.parents(~K, r), q, M.nparent(~K, y)), NR.parents(~K, SC.update(M.Node<K>, r, q, y)), parents_upd(~K, r, q, y))
438	
439	def parents_snoc(~K: Data, +xs: List<&2, M.Node<K>>, +y: M.Node<K>) -> {SC.snoc(Nat, NR.parents(~K, xs), M.nparent(~K, y)) == NR.parents(~K, SC.snoc(M.Node<K>, xs, y)) : List<&2, Nat>}:
440	  match xs:
441	    case Nil{}:
442	      {==}
443	    case Con{+x, +r}:
444	      LL.cons_cong(Nat, M.nparent(~K, x), SC.snoc(Nat, NR.parents(~K, r), M.nparent(~K, y)), NR.parents(~K, SC.snoc(M.Node<K>, r, y)), parents_snoc(~K, r, y))
445	
446	def parents_init(~K: Data, +xs: List<&2, M.Node<K>>) -> {SC.init(Nat, NR.parents(~K, xs)) == NR.parents(~K, SC.init(M.Node<K>, xs)) : List<&2, Nat>}:
447	  match xs:
448	    case Nil{}:
449	      {==}
450	    case Con{x, Nil{}}:
451	      {==}
452	    case Con{+x, Con{+y, +t}}:
453	      LL.cons_cong(Nat, M.nparent(~K, x), SC.init(Nat, NR.parents(~K, Con{y, t})), NR.parents(~K, SC.init(M.Node<K>, Con{y, t})), parents_init(~K, Con{y, t}))
454	
455	# the field block: a slot below the length reads the field
456	def parent_get(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +y: M.Node<K>, +hy: {SC.nth(M.Node<K>, xs, i) == Some{y} : Maybe<&2, M.Node<K>>}) -> {Array.get(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), U32.from_nat(i)) == (AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), M.nparent(~K, y)) : Array<Nat> & Nat}:
457	  +fl = NR.parents(~K, xs)
458	  +t = BK.bk(Nat, d, fl, 0n)
459	  +hlen = parents_len(~K, xs)
460	  +hi = LL.nth_lt_length(M.Node<K>, xs, i, y, hy)
461	  +hip = N.lt_le_trans(i, SC.length(M.Node<K>, xs), SC.pow2(d), hi, hc)
462	  +eu = U.to_nat_from_nat(i, d, DAS.le32(d, l, hd, hl), hip)
463	  +hiF = L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hi)
464	  +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hc)
465	  +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), i), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), Some{M.nparent(~K, y)}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, i), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), SC.nth(Nat, fl, i), Some{M.nparent(~K, y)}, BK.fill_nth(Nat, SC.pow2(d), fl, 0n, i, hiF, hcF), parents_nth(~K, xs, i, y, hy)))
466	  +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{M.nparent(~K, y)} : Maybe<&2, Nat>}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hx0)
467	  +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hip)
468	  AR.get(Nat, d, t, U32.from_nat(i), M.nparent(~K, y), DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))
469	
470	# a slot below the length written with a node's field
471	def parent_set(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +y0: M.Node<K>, +hy0: {SC.nth(M.Node<K>, xs, i) == Some{y0} : Maybe<&2, M.Node<K>>}, +y: M.Node<K>) -> {Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), U32.from_nat(i), M.nparent(~K, y)) == AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, y)), 0n)) : Array<Nat>}:
472	  +fl = NR.parents(~K, xs)
473	  +t = BK.bk(Nat, d, fl, 0n)
474	  +hlen = parents_len(~K, xs)
475	  +hi = LL.nth_lt_length(M.Node<K>, xs, i, y0, hy0)
476	  +hip = N.lt_le_trans(i, SC.length(M.Node<K>, xs), SC.pow2(d), hi, hc)
477	  +eu = U.to_nat_from_nat(i, d, DAS.le32(d, l, hd, hl), hip)
478	  +hiF = L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hi)
479	  +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hc)
480	  +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), i), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), Some{M.nparent(~K, y0)}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, i), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), SC.nth(Nat, fl, i), Some{M.nparent(~K, y0)}, BK.fill_nth(Nat, SC.pow2(d), fl, 0n, i, hiF, hcF), parents_nth(~K, xs, i, y0, hy0)))
481	  +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{M.nparent(~K, y0)} : Maybe<&2, Nat>}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hx0)
482	  +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hip)
483	  %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, t), U32.from_nat(i), M.nparent(~K, y)), AR.thaw(Nat, AR.upd(Nat, d, t, U32.to_nat(U32.from_nat(i)), M.nparent(~K, y))), AR.set(Nat, d, t, U32.from_nat(i), M.nparent(~K, y), M.nparent(~K, y0), DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))) : {_ == AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, y)), 0n)) : Array<Nat>}
484	  %Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu) : {AR.thaw(Nat, AR.upd(Nat, d, t, _, M.nparent(~K, y))) == AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, y)), 0n)) : Array<Nat>}
485	  Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.upd(Nat, d, t, i, M.nparent(~K, y)), BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, y)), 0n), Equal.trans(AR.Tree<Nat>, AR.upd(Nat, d, t, i, M.nparent(~K, y)), BK.bk(Nat, d, SC.update(Nat, fl, i, M.nparent(~K, y)), 0n), BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, y)), 0n), BK.bk_set(Nat, d, fl, 0n, i, M.nparent(~K, y), hiF, hcF), Equal.cong(List<&2, Nat>, AR.Tree<Nat>, z => BK.bk(Nat, d, z, 0n), SC.update(Nat, fl, i, M.nparent(~K, y)), NR.parents(~K, SC.update(M.Node<K>, xs, i, y)), parents_upd(~K, xs, i, y))))
486	
487	# the slot at the length (inside the capacity) written: an append
488	def parent_push(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +y: M.Node<K>, +hn: {Nat.is_lt(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}) -> {Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), U32.from_nat(SC.length(M.Node<K>, xs)), M.nparent(~K, y)) == AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}:
489	  +fl = NR.parents(~K, xs)
490	  +t = BK.bk(Nat, d, fl, 0n)
491	  +n = SC.length(M.Node<K>, xs)
492	  +hlen = parents_len(~K, xs)
493	  +eu = U.to_nat_from_nat(n, d, DAS.le32(d, l, hd, hl), hn)
494	  +hnF = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, n, SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), n, hlen), hn)
495	  +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), SC.length(Nat, fl)), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), SC.length(Nat, fl)), Some{0n}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, SC.length(Nat, fl)), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), BK.fill_at_len(Nat, SC.pow2(d), fl, 0n, hnF))
496	  +hx1 = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{0n} : Maybe<&2, Nat>}, SC.length(Nat, fl), n, hlen, hx0)
497	  +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{0n} : Maybe<&2, Nat>}, n, U32.to_nat(U32.from_nat(n)), Equal.sym(Nat, U32.to_nat(U32.from_nat(n)), n, eu), hx1)
498	  +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, n, U32.to_nat(U32.from_nat(n)), Equal.sym(Nat, U32.to_nat(U32.from_nat(n)), n, eu), hn)
499	  %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, t), U32.from_nat(n), M.nparent(~K, y)), AR.thaw(Nat, AR.upd(Nat, d, t, U32.to_nat(U32.from_nat(n)), M.nparent(~K, y))), AR.set(Nat, d, t, U32.from_nat(n), M.nparent(~K, y), 0n, DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))) : {_ == AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}
500	  %Equal.sym(Nat, U32.to_nat(U32.from_nat(n)), n, eu) : {AR.thaw(Nat, AR.upd(Nat, d, t, _, M.nparent(~K, y))) == AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}
501	  %hlen : {AR.thaw(Nat, AR.upd(Nat, d, t, _, M.nparent(~K, y))) == AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}
502	  Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.upd(Nat, d, t, SC.length(Nat, fl), M.nparent(~K, y)), BK.bk(Nat, d, NR.parents(~K, SC.snoc(M.Node<K>, xs, y)), 0n), Equal.trans(AR.Tree<Nat>, AR.upd(Nat, d, t, SC.length(Nat, fl), M.nparent(~K, y)), BK.bk(Nat, d, SC.snoc(Nat, fl, M.nparent(~K, y)), 0n), BK.bk(Nat, d, NR.parents(~K, SC.snoc(M.Node<K>, xs, y)), 0n), BK.bk_push(Nat, d, fl, 0n, M.nparent(~K, y), hnF), Equal.cong(List<&2, Nat>, AR.Tree<Nat>, z => BK.bk(Nat, d, z, 0n), SC.snoc(Nat, fl, M.nparent(~K, y)), NR.parents(~K, SC.snoc(M.Node<K>, xs, y)), parents_snoc(~K, xs, y))))
503	
504	# the block doubled with a default half
505	def parent_grow(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}) -> {ANode{AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), Array.new(Nat, d, 0n)} == AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.parents(~K, xs), 0n)) : Array<Nat>}:
506	  +fl = NR.parents(~K, xs)
507	  +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), parents_len(~K, xs)), hc)
508	  %Equal.sym(Array<Nat>, Array.new(Nat, d, 0n), AR.thaw(Nat, AR.trep(Nat, d, 0n)), AR.new(Nat, d, 0n)) : {ANode{AR.thaw(Nat, BK.bk(Nat, d, fl, 0n)), _} == AR.thaw(Nat, BK.bk(Nat, 1n+d, fl, 0n)) : Array<Nat>}
509	  Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.TNode{BK.bk(Nat, d, fl, 0n), AR.trep(Nat, d, 0n)}, BK.bk(Nat, 1n+d, fl, 0n), BK.bk_grow(Nat, d, fl, 0n, hcF))
510	
511	# the last slot reset to the encoding of Free{0}: a pop
512	def parent_drop(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +m: Nat, +hm: {SC.length(M.Node<K>, xs) == 1n+m : Nat}, +y0: M.Node<K>, +hy0: {SC.nth(M.Node<K>, xs, m) == Some{y0} : Maybe<&2, M.Node<K>>}) -> {Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), U32.from_nat(m), M.nparent(~K, M.Free{0n})) == AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.init(M.Node<K>, xs)), 0n)) : Array<Nat>}:
513	  +fl = NR.parents(~K, xs)
514	  +t = BK.bk(Nat, d, fl, 0n)
515	  +hlen = parents_len(~K, xs)
516	  +hi = LL.nth_lt_length(M.Node<K>, xs, m, y0, hy0)
517	  +hip = N.lt_le_trans(m, SC.length(M.Node<K>, xs), SC.pow2(d), hi, hc)
518	  +eu = U.to_nat_from_nat(m, d, DAS.le32(d, l, hd, hl), hip)
519	  +hiF = L.subst(Nat, z => {Nat.is_lt(m, z) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hi)
520	  +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hc)
521	  +hmF = Equal.trans(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), 1n+m, hlen, hm)
522	  +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), m), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), m), Some{M.nparent(~K, y0)}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, m), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), m), SC.nth(Nat, fl, m), Some{M.nparent(~K, y0)}, BK.fill_nth(Nat, SC.pow2(d), fl, 0n, m, hiF, hcF), parents_nth(~K, xs, m, y0, hy0)))
523	  +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{M.nparent(~K, y0)} : Maybe<&2, Nat>}, m, U32.to_nat(U32.from_nat(m)), Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, eu), hx0)
524	  +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, m, U32.to_nat(U32.from_nat(m)), Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, eu), hip)
525	  %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, t), U32.from_nat(m), 0n), AR.thaw(Nat, AR.upd(Nat, d, t, U32.to_nat(U32.from_nat(m)), 0n)), AR.set(Nat, d, t, U32.from_nat(m), 0n, M.nparent(~K, y0), DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))) : {_ == AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.init(M.Node<K>, xs)), 0n)) : Array<Nat>}
526	  %Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, eu) : {AR.thaw(Nat, AR.upd(Nat, d, t, _, 0n)) == AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.init(M.Node<K>, xs)), 0n)) : Array<Nat>}
527	  Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.upd(Nat, d, t, m, 0n), BK.bk(Nat, d, NR.parents(~K, SC.init(M.Node<K>, xs)), 0n), Equal.trans(AR.Tree<Nat>, AR.upd(Nat, d, t, m, 0n), BK.bk(Nat, d, SC.init(Nat, fl), 0n), BK.bk(Nat, d, NR.parents(~K, SC.init(M.Node<K>, xs)), 0n), BK.bk_pop(Nat, d, fl, 0n, m, hmF, hcF), Equal.cong(List<&2, Nat>, AR.Tree<Nat>, z => BK.bk(Nat, d, z, 0n), SC.init(Nat, fl), NR.parents(~K, SC.init(M.Node<K>, xs)), parents_init(~K, xs))))
528	
529	# updating a node that keeps this field leaves the field list
530	def parents_keep(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>, +x: M.Node<K>, +hy: {SC.nth(M.Node<K>, xs, i) == Some{y} : Maybe<&2, M.Node<K>>}, +he: {M.nparent(~K, x) == M.nparent(~K, y) : Nat}) -> {NR.parents(~K, SC.update(M.Node<K>, xs, i, x)) == NR.parents(~K, xs) : List<&2, Nat>}:
531	  %parents_upd(~K, xs, i, x) : {_ == NR.parents(~K, xs) : List<&2, Nat>}
532	  %Equal.sym(Nat, M.nparent(~K, x), M.nparent(~K, y), he) : {SC.update(Nat, NR.parents(~K, xs), i, _) == NR.parents(~K, xs) : List<&2, Nat>}
533	  upd_same(Nat, NR.parents(~K, xs), i, M.nparent(~K, y), parents_nth(~K, xs, i, y, hy))
534	
535	def keys_len(~K: Data, +xs: List<&2, M.Node<K>>) -> {SC.length(Maybe<&2, K>, NR.keys(~K, xs)) == SC.length(M.Node<K>, xs) : Nat}:
536	  match xs:
537	    case Nil{}:
538	      {==}
539	    case Con{x, +r}:
540	      N.succ_cong(SC.length(Maybe<&2, K>, NR.keys(~K, r)), SC.length(M.Node<K>, r), keys_len(~K, r))
541	
542	def keys_nth(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>, +h: {SC.nth(M.Node<K>, xs, i) == Some{y} : Maybe<&2, M.Node<K>>}) -> {SC.nth(Maybe<&2, K>, NR.keys(~K, xs), i) == Some{M.nkey(~K, y)} : Maybe<&2, Maybe<&2, K>>}:
543	  match xs i:
544	    case Nil{} _:
545	      Empty.absurd({SC.nth(Maybe<&2, K>, Nil{}, i) == Some{M.nkey(~K, y)} : Maybe<&2, Maybe<&2, K>>}, L.false_true(Equal.cong(Maybe<&2, M.Node<K>>, Bool, z => mb(~K, z), None{}, Some{y}, h)))
546	    case Con{+x, r} 0n:
547	      Equal.cong(Maybe<&2, M.Node<K>>, Maybe<&2, Maybe<&2, K>>, z => Some{M.nkey(~K, unsome(~K, z, x))}, Some{x}, Some{y}, h)
548	    case Con{x, +r} 1n+q:
549	      keys_nth(~K, r, q, y, h)
550	
551	def keys_upd(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>) -> {SC.update(Maybe<&2, K>, NR.keys(~K, xs), i, M.nkey(~K, y)) == NR.keys(~K, SC.update(M.Node<K>, xs, i, y)) : List<&2, Maybe<&2, K>>}:
552	  match xs i:
553	    case Nil{} _:
554	      {==}
555	    case Con{x, r} 0n:
556	      {==}
557	    case Con{+x, +r} 1n+q:
558	      LL.cons_cong(Maybe<&2, K>, M.nkey(~K, x), SC.update(Maybe<&2, K>, NR.keys(~K, r), q, M.nkey(~K, y)), NR.keys(~K, SC.update(M.Node<K>, r, q, y)), keys_upd(~K, r, q, y))
559	
560	def keys_snoc(~K: Data, +xs: List<&2, M.Node<K>>, +y: M.Node<K>) -> {SC.snoc(Maybe<&2, K>, NR.keys(~K, xs), M.nkey(~K, y)) == NR.keys(~K, SC.snoc(M.Node<K>, xs, y)) : List<&2, Maybe<&2, K>>}:
561	  match xs:
562	    case Nil{}:
563	      {==}
564	    case Con{+x, +r}:
565	      LL.cons_cong(Maybe<&2, K>, M.nkey(~K, x), SC.snoc(Maybe<&2, K>, NR.keys(~K, r), M.nkey(~K, y)), NR.keys(~K, SC.snoc(M.Node<K>, r, y)), keys_snoc(~K, r, y))
566	
567	def keys_init(~K: Data, +xs: List<&2, M.Node<K>>) -> {SC.init(Maybe<&2, K>, NR.keys(~K, xs)) == NR.keys(~K, SC.init(M.Node<K>, xs)) : List<&2, Maybe<&2, K>>}:
568	  match xs:
569	    case Nil{}:
570	      {==}
571	    case Con{x, Nil{}}:
572	      {==}
573	    case Con{+x, Con{+y, +t}}:
574	      LL.cons_cong(Maybe<&2, K>, M.nkey(~K, x), SC.init(Maybe<&2, K>, NR.keys(~K, Con{y, t})), NR.keys(~K, SC.init(M.Node<K>, Con{y, t})), keys_init(~K, Con{y, t}))
575	
576	# the field block: a slot below the length reads the field
577	def key_get(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +y: M.Node<K>, +hy: {SC.nth(M.Node<K>, xs, i) == Some{y} : Maybe<&2, M.Node<K>>}) -> {Array.get(Maybe<&2, K>, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(i)) == (AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), M.nkey(~K, y)) : Array<Maybe<&2, K>> & Maybe<&2, K>}:
578	  +fl = NR.keys(~K, xs)
579	  +t = BK.bk(Maybe<&2, K>, d, fl, None{})
580	  +hlen = keys_len(~K, xs)
581	  +hi = LL.nth_lt_length(M.Node<K>, xs, i, y, hy)
582	  +hip = N.lt_le_trans(i, SC.length(M.Node<K>, xs), SC.pow2(d), hi, hc)
583	  +eu = U.to_nat_from_nat(i, d, DAS.le32(d, l, hd, hl), hip)
584	  +hiF = L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Maybe<&2, K>, fl), Equal.sym(Nat, SC.length(Maybe<&2, K>, fl), SC.length(M.Node<K>, xs), hlen), hi)
585	  +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Maybe<&2, K>, fl), Equal.sym(Nat, SC.length(Maybe<&2, K>, fl), SC.length(M.Node<K>, xs), hlen), hc)
586	  +hx0 = Equal.trans(Maybe<&2, Maybe<&2, K>>, SC.nth(Maybe<&2, K>, AR.slots(Maybe<&2, K>, t), i), SC.nth(Maybe<&2, K>, BK.fillv(Maybe<&2, K>, SC.pow2(d), fl, None{}), i), Some{M.nkey(~K, y)}, Equal.cong(List<&2, Maybe<&2, K>>, Maybe<&2, Maybe<&2, K>>, z => SC.nth(Maybe<&2, K>, z, i), AR.slots(Maybe<&2, K>, t), BK.fillv(Maybe<&2, K>, SC.pow2(d), fl, None{}), BK.bk_slots(Maybe<&2, K>, d, fl, None{})), Equal.trans(Maybe<&2, Maybe<&2, K>>, SC.nth(Maybe<&2, K>, BK.fillv(Maybe<&2, K>, SC.pow2(d), fl, None{}), i), SC.nth(Maybe<&2, K>, fl, i), Some{M.nkey(~K, y)}, BK.fill_nth(Maybe<&2, K>, SC.pow2(d), fl, None{}, i, hiF, hcF), keys_nth(~K, xs, i, y, hy)))
587	  +hx = L.subst(Nat, z => {SC.nth(Maybe<&2, K>, AR.slots(Maybe<&2, K>, t), z) == Some{M.nkey(~K, y)} : Maybe<&2, Maybe<&2, K>>}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hx0)
588	  +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hip)
589	  AR.get(Maybe<&2, K>, d, t, U32.from_nat(i), M.nkey(~K, y), DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Maybe<&2, K>, d, fl, None{}))
590	
591	# a slot below the length written with a node's field
592	def key_set(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +y0: M.Node<K>, +hy0: {SC.nth(M.Node<K>, xs, i) == Some{y0} : Maybe<&2, M.Node<K>>}, +y: M.Node<K>) -> {Array.set(Maybe<&2, K>, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(i), M.nkey(~K, y)) == AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, y)), None{})) : Array<Maybe<&2, K>>}:
593	  +fl = NR.keys(~K, xs)
594	  +t = BK.bk(Maybe<&2, K>, d, fl, None{})
595	  +hlen = keys_len(~K, xs)
596	  +hi = LL.nth_lt_length(M.Node<K>, xs, i, y0, hy0)
597	  +hip = N.lt_le_trans(i, SC.length(M.Node<K>, xs), SC.pow2(d), hi, hc)
598	  +eu = U.to_nat_from_nat(i, d, DAS.le32(d, l, hd, hl), hip)
599	  +hiF = L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Maybe<&2, K>, fl), Equal.sym(Nat, SC.length(Maybe<&2, K>, fl), SC.length(M.Node<K>, xs), hlen), hi)
600	  +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Maybe<&2, K>, fl), Equal.sym(Nat, SC.length(Maybe<&2, K>, fl), SC.length(M.Node<K>, xs), hlen), hc)
601	  +hx0 = Equal.trans(Maybe<&2, Maybe<&2, K>>, SC.nth(Maybe<&2, K>, AR.slots(Maybe<&2, K>, t), i), SC.nth(Maybe<&2, K>, BK.fillv(Maybe<&2, K>, SC.pow2(d), fl, None{}), i), Some{M.nkey(~K, y0)}, Equal.cong(List<&2, Maybe<&2, K>>, Maybe<&2, Maybe<&2, K>>, z => SC.nth(Maybe<&2, K>, z, i), AR.slots(Maybe<&2, K>, t), BK.fillv(Maybe<&2, K>, SC.pow2(d), fl, None{}), BK.bk_slots(Maybe<&2, K>, d, fl, None{})), Equal.trans(Maybe<&2, Maybe<&2, K>>, SC.nth(Maybe<&2, K>, BK.fillv(Maybe<&2, K>, SC.pow2(d), fl, None{}), i), SC.nth(Maybe<&2, K>, fl, i), Some{M.nkey(~K, y0)}, BK.fill_nth(Maybe<&2, K>, SC.pow2(d), fl, None{}, i, hiF, hcF), keys_nth(~K, xs, i, y0, hy0)))
602	  +hx = L.subst(Nat, z => {SC.nth(Maybe<&2, K>, AR.slots(Maybe<&2, K>, t), z) == Some{M.nkey(~K, y0)} : Maybe<&2, Maybe<&2, K>>}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hx0)
603	  +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hip)
604	  %Equal.sym(Array<Maybe<&2, K>>, Array.set(Maybe<&2, K>, AR.thaw(Maybe<&2, K>, t), U32.from_nat(i), M.nkey(~K, y)), AR.thaw(Maybe<&2, K>, AR.upd(Maybe<&2, K>, d, t, U32.to_nat(U32.from_nat(i)), M.nkey(~K, y))), AR.set(Maybe<&2, K>, d, t, U32.from_nat(i), M.nkey(~K, y), M.nkey(~K, y0), DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Maybe<&2, K>, d, fl, None{}))) : {_ == AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, y)), None{})) : Array<Maybe<&2, K>>}
605	  %Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu) : {AR.thaw(Maybe<&2, K>, AR.upd(Maybe<&2, K>, d, t, _, M.nkey(~K, y))) == AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, y)), None{})) : Array<Maybe<&2, K>>}
606	  Equal.cong(AR.Tree<Maybe<&2, K>>, Array<Maybe<&2, K>>, z => AR.thaw(Maybe<&2, K>, z), AR.upd(Maybe<&2, K>, d, t, i, M.nkey(~K, y)), BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, y)), None{}), Equal.trans(AR.Tree<Maybe<&2, K>>, AR.upd(Maybe<&2, K>, d, t, i, M.nkey(~K, y)), BK.bk(Maybe<&2, K>, d, SC.update(Maybe<&2, K>, fl, i, M.nkey(~K, y)), None{}), BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, y)), None{}), BK.bk_set(Maybe<&2, K>, d, fl, None{}, i, M.nkey(~K, y), hiF, hcF), Equal.cong(List<&2, Maybe<&2, K>>, AR.Tree<Maybe<&2, K>>, z => BK.bk(Maybe<&2, K>, d, z, None{}), SC.update(Maybe<&2, K>, fl, i, M.nkey(~K, y)), NR.keys(~K, SC.update(M.Node<K>, xs, i, y)), keys_upd(~K, xs, i, y))))
607	
608	# the slot at the length (inside the capacity) written: an append
609	def key_push(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +y: M.Node<K>, +hn: {Nat.is_lt(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}) -> {Array.set(Maybe<&2, K>, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(SC.length(M.Node<K>, xs)), M.nkey(~K, y)) == AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.snoc(M.Node<K>, xs, y)), None{})) : Array<Maybe<&2, K>>}:
610	  +fl = NR.keys(~K, xs)
611	  +t = BK.bk(Maybe<&2, K>, d, fl, None{})
612	  +n = SC.length(M.Node<K>, xs)
613	  +hlen = keys_len(~K, xs)
614	  +eu = U.to_nat_from_nat(n, d, DAS.le32(d, l, hd, hl), hn)
615	  +hnF = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, n, SC.length(Maybe<&2, K>, fl), Equal.sym(Nat, SC.length(Maybe<&2, K>, fl), n, hlen), hn)
616	  +hx0 = Equal.trans(Maybe<&2, Maybe<&2, K>>, SC.nth(Maybe<&2, K>, AR.slots(Maybe<&2, K>, t), SC.length(Maybe<&2, K>, fl)), SC.nth(Maybe<&2, K>, BK.fillv(Maybe<&2, K>, SC.pow2(d), fl, None{}), SC.length(Maybe<&2, K>, fl)), Some{None{}}, Equal.cong(List<&2, Maybe<&2, K>>, Maybe<&2, Maybe<&2, K>>, z => SC.nth(Maybe<&2, K>, z, SC.length(Maybe<&2, K>, fl)), AR.slots(Maybe<&2, K>, t), BK.fillv(Maybe<&2, K>, SC.pow2(d), fl, None{}), BK.bk_slots(Maybe<&2, K>, d, fl, None{})), BK.fill_at_len(Maybe<&2, K>, SC.pow2(d), fl, None{}, hnF))
617	  +hx1 = L.subst(Nat, z => {SC.nth(Maybe<&2, K>, AR.slots(Maybe<&2, K>, t), z) == Some{None{}} : Maybe<&2, Maybe<&2, K>>}, SC.length(Maybe<&2, K>, fl), n, hlen, hx0)
618	  +hx = L.subst(Nat, z => {SC.nth(Maybe<&2, K>, AR.slots(Maybe<&2, K>, t), z) == Some{None{}} : Maybe<&2, Maybe<&2, K>>}, n, U32.to_nat(U32.from_nat(n)), Equal.sym(Nat, U32.to_nat(U32.from_nat(n)), n, eu), hx1)
619	  +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, n, U32.to_nat(U32.from_nat(n)), Equal.sym(Nat, U32.to_nat(U32.from_nat(n)), n, eu), hn)
620	  %Equal.sym(Array<Maybe<&2, K>>, Array.set(Maybe<&2, K>, AR.thaw(Maybe<&2, K>, t), U32.from_nat(n), M.nkey(~K, y)), AR.thaw(Maybe<&2, K>, AR.upd(Maybe<&2, K>, d, t, U32.to_nat(U32.from_nat(n)), M.nkey(~K, y))), AR.set(Maybe<&2, K>, d, t, U32.from_nat(n), M.nkey(~K, y), None{}, DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Maybe<&2, K>, d, fl, None{}))) : {_ == AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.snoc(M.Node<K>, xs, y)), None{})) : Array<Maybe<&2, K>>}
621	  %Equal.sym(Nat, U32.to_nat(U32.from_nat(n)), n, eu) : {AR.thaw(Maybe<&2, K>, AR.upd(Maybe<&2, K>, d, t, _, M.nkey(~K, y))) == AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.snoc(M.Node<K>, xs, y)), None{})) : Array<Maybe<&2, K>>}
622	  %hlen : {AR.thaw(Maybe<&2, K>, AR.upd(Maybe<&2, K>, d, t, _, M.nkey(~K, y))) == AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.snoc(M.Node<K>, xs, y)), None{})) : Array<Maybe<&2, K>>}
623	  Equal.cong(AR.Tree<Maybe<&2, K>>, Array<Maybe<&2, K>>, z => AR.thaw(Maybe<&2, K>, z), AR.upd(Maybe<&2, K>, d, t, SC.length(Maybe<&2, K>, fl), M.nkey(~K, y)), BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.snoc(M.Node<K>, xs, y)), None{}), Equal.trans(AR.Tree<Maybe<&2, K>>, AR.upd(Maybe<&2, K>, d, t, SC.length(Maybe<&2, K>, fl), M.nkey(~K, y)), BK.bk(Maybe<&2, K>, d, SC.snoc(Maybe<&2, K>, fl, M.nkey(~K, y)), None{}), BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.snoc(M.Node<K>, xs, y)), None{}), BK.bk_push(Maybe<&2, K>, d, fl, None{}, M.nkey(~K, y), hnF), Equal.cong(List<&2, Maybe<&2, K>>, AR.Tree<Maybe<&2, K>>, z => BK.bk(Maybe<&2, K>, d, z, None{}), SC.snoc(Maybe<&2, K>, fl, M.nkey(~K, y)), NR.keys(~K, SC.snoc(M.Node<K>, xs, y)), keys_snoc(~K, xs, y))))
624	
625	# the block doubled with a default half
626	def key_grow(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}) -> {ANode{AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), Array.new(Maybe<&2, K>, d, None{})} == AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, 1n+d, NR.keys(~K, xs), None{})) : Array<Maybe<&2, K>>}:
627	  +fl = NR.keys(~K, xs)
628	  +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Maybe<&2, K>, fl), Equal.sym(Nat, SC.length(Maybe<&2, K>, fl), SC.length(M.Node<K>, xs), keys_len(~K, xs)), hc)
629	  %Equal.sym(Array<Maybe<&2, K>>, Array.new(Maybe<&2, K>, d, None{}), AR.thaw(Maybe<&2, K>, AR.trep(Maybe<&2, K>, d, None{})), AR.new(Maybe<&2, K>, d, None{})) : {ANode{AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, fl, None{})), _} == AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, 1n+d, fl, None{})) : Array<Maybe<&2, K>>}
630	  Equal.cong(AR.Tree<Maybe<&2, K>>, Array<Maybe<&2, K>>, z => AR.thaw(Maybe<&2, K>, z), AR.TNode{BK.bk(Maybe<&2, K>, d, fl, None{}), AR.trep(Maybe<&2, K>, d, None{})}, BK.bk(Maybe<&2, K>, 1n+d, fl, None{}), BK.bk_grow(Maybe<&2, K>, d, fl, None{}, hcF))
631	
632	# the last slot reset to the encoding of Free{0}: a pop
633	def key_drop(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +m: Nat, +hm: {SC.length(M.Node<K>, xs) == 1n+m : Nat}, +y0: M.Node<K>, +hy0: {SC.nth(M.Node<K>, xs, m) == Some{y0} : Maybe<&2, M.Node<K>>}) -> {Array.set(Maybe<&2, K>, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(m), M.nkey(~K, M.Free{0n})) == AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.init(M.Node<K>, xs)), None{})) : Array<Maybe<&2, K>>}:
634	  +fl = NR.keys(~K, xs)
635	  +t = BK.bk(Maybe<&2, K>, d, fl, None{})
636	  +hlen = keys_len(~K, xs)
637	  +hi = LL.nth_lt_length(M.Node<K>, xs, m, y0, hy0)
638	  +hip = N.lt_le_trans(m, SC.length(M.Node<K>, xs), SC.pow2(d), hi, hc)
639	  +eu = U.to_nat_from_nat(m, d, DAS.le32(d, l, hd, hl), hip)
640	  +hiF = L.subst(Nat, z => {Nat.is_lt(m, z) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Maybe<&2, K>, fl), Equal.sym(Nat, SC.length(Maybe<&2, K>, fl), SC.length(M.Node<K>, xs), hlen), hi)
641	  +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Maybe<&2, K>, fl), Equal.sym(Nat, SC.length(Maybe<&2, K>, fl), SC.length(M.Node<K>, xs), hlen), hc)
642	  +hmF = Equal.trans(Nat, SC.length(Maybe<&2, K>, fl), SC.length(M.Node<K>, xs), 1n+m, hlen, hm)
643	  +hx0 = Equal.trans(Maybe<&2, Maybe<&2, K>>, SC.nth(Maybe<&2, K>, AR.slots(Maybe<&2, K>, t), m), SC.nth(Maybe<&2, K>, BK.fillv(Maybe<&2, K>, SC.pow2(d), fl, None{}), m), Some{M.nkey(~K, y0)}, Equal.cong(List<&2, Maybe<&2, K>>, Maybe<&2, Maybe<&2, K>>, z => SC.nth(Maybe<&2, K>, z, m), AR.slots(Maybe<&2, K>, t), BK.fillv(Maybe<&2, K>, SC.pow2(d), fl, None{}), BK.bk_slots(Maybe<&2, K>, d, fl, None{})), Equal.trans(Maybe<&2, Maybe<&2, K>>, SC.nth(Maybe<&2, K>, BK.fillv(Maybe<&2, K>, SC.pow2(d), fl, None{}), m), SC.nth(Maybe<&2, K>, fl, m), Some{M.nkey(~K, y0)}, BK.fill_nth(Maybe<&2, K>, SC.pow2(d), fl, None{}, m, hiF, hcF), keys_nth(~K, xs, m, y0, hy0)))
644	  +hx = L.subst(Nat, z => {SC.nth(Maybe<&2, K>, AR.slots(Maybe<&2, K>, t), z) == Some{M.nkey(~K, y0)} : Maybe<&2, Maybe<&2, K>>}, m, U32.to_nat(U32.from_nat(m)), Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, eu), hx0)
645	  +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, m, U32.to_nat(U32.from_nat(m)), Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, eu), hip)
646	  %Equal.sym(Array<Maybe<&2, K>>, Array.set(Maybe<&2, K>, AR.thaw(Maybe<&2, K>, t), U32.from_nat(m), None{}), AR.thaw(Maybe<&2, K>, AR.upd(Maybe<&2, K>, d, t, U32.to_nat(U32.from_nat(m)), None{})), AR.set(Maybe<&2, K>, d, t, U32.from_nat(m), None{}, M.nkey(~K, y0), DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Maybe<&2, K>, d, fl, None{}))) : {_ == AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.init(M.Node<K>, xs)), None{})) : Array<Maybe<&2, K>>}
647	  %Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, eu) : {AR.thaw(Maybe<&2, K>, AR.upd(Maybe<&2, K>, d, t, _, None{})) == AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.init(M.Node<K>, xs)), None{})) : Array<Maybe<&2, K>>}
648	  Equal.cong(AR.Tree<Maybe<&2, K>>, Array<Maybe<&2, K>>, z => AR.thaw(Maybe<&2, K>, z), AR.upd(Maybe<&2, K>, d, t, m, None{}), BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.init(M.Node<K>, xs)), None{}), Equal.trans(AR.Tree<Maybe<&2, K>>, AR.upd(Maybe<&2, K>, d, t, m, None{}), BK.bk(Maybe<&2, K>, d, SC.init(Maybe<&2, K>, fl), None{}), BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.init(M.Node<K>, xs)), None{}), BK.bk_pop(Maybe<&2, K>, d, fl, None{}, m, hmF, hcF), Equal.cong(List<&2, Maybe<&2, K>>, AR.Tree<Maybe<&2, K>>, z => BK.bk(Maybe<&2, K>, d, z, None{}), SC.init(Maybe<&2, K>, fl), NR.keys(~K, SC.init(M.Node<K>, xs)), keys_init(~K, xs))))
649	
650	# updating a node that keeps this field leaves the field list
651	def keys_keep(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>, +x: M.Node<K>, +hy: {SC.nth(M.Node<K>, xs, i) == Some{y} : Maybe<&2, M.Node<K>>}, +he: {M.nkey(~K, x) == M.nkey(~K, y) : Maybe<&2, K>}) -> {NR.keys(~K, SC.update(M.Node<K>, xs, i, x)) == NR.keys(~K, xs) : List<&2, Maybe<&2, K>>}:
652	  %keys_upd(~K, xs, i, x) : {_ == NR.keys(~K, xs) : List<&2, Maybe<&2, K>>}
653	  %Equal.sym(Maybe<&2, K>, M.nkey(~K, x), M.nkey(~K, y), he) : {SC.update(Maybe<&2, K>, NR.keys(~K, xs), i, _) == NR.keys(~K, xs) : List<&2, Maybe<&2, K>>}
654	  upd_same(Maybe<&2, K>, NR.keys(~K, xs), i, M.nkey(~K, y), keys_nth(~K, xs, i, y, hy))
655