1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/list.bend as LL
4	import ../../lib/order.bend as O
5	import ../../../spec/lib/common.bend as SC
6	import ../../../spec/containers/balanced_search_tree/main.bend as S
7	import ../../../src/containers/balanced_search_tree.bend as M
8	import ./state.bend as ST
9	import ./mirror.bend as MI
10	import ./ord.bend as OR
11	import ./dord.bend as DO
12	import ./cur.bend as CU
13	import ./vsp.bend as VS
14	import ./vsz.bend as VZ
15	import ./vdef.bend as VD
16	
17	# A view's clear: the implementation walks the view's cursor, removing each
18	# entry in range, until one is out of range; each step is the specification
19	# cursor's, so what is left is the entries outside the view.
20	# (source: tools/generators/tm_hand/vclr.src)
21	
22	
23	# ---- the cursor's view ----
24	
25	def vw_of(-K: Data, -V: Data, c: S.Cursor<K, V>) -> S.View<K, V>:
26	  match c:
27	    case S.CR{m, nx, cu, lo, hi, fw}:
28	      S.VW{m, lo, hi, Bool.not(fw)}
29	
30	def iv_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +c2: MI.MCursor<K, V>, +hc2: {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool}) -> VD.VOK(~K, ~V, ~cmp, vw_of(K, V, CU.cmod(~K, ~V, ~cmp, c2)), M.iterator_view(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2))):
31	  match c2:
32	    case MI.MC{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +a, +b, +lo3, +hi3, +fw3}:
33	      (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo3, hi3, Bool.not(fw3)}, ({==}, ({==}, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), a), Bool.and(CU.idok(ST.ids(tg), b), Bool.or(Nat.is_eq(a, 0n), Bool.not(Nat.is_eq(a, b))))), hc2))))
34	
35	def is_nil(-A: Data, xs: List<&2, A>) -> Bool:
36	  match xs:
37	    case Nil{}:
38	      True{}
39	    case Con{h, t}:
40	      False{}
41	
42	def con_nil(-A: Data, +x: A, +t: List<&2, A>, +h: {Con{x, t} == Nil{} : List<&2, A>}) -> Empty:
43	  L.false_true(VS.cong(List<&2, A>, Bool, z => is_nil(A, z), Con{x, t}, Nil{}, h))
44	
45	# nothing within: nothing to clear
46	def oid_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +h: {S.within(~K, ~V, ~cmp, lo2, hi2, Con{e, t}) == Nil{} : List<&2, M.Entry<K, V>>}, +b: Bool, +hb: {S.in_range(~K, ~cmp, S.key(K, V, e), lo2, hi2) == b : Bool}, kf: @+ht: {S.within(~K, ~V, ~cmp, lo2, hi2, t) == Nil{} : List<&2, M.Entry<K, V>>} -> {S.outside(~K, ~V, ~cmp, lo2, hi2, t) == t : List<&2, M.Entry<K, V>>}) -> {S.outside(~K, ~V, ~cmp, lo2, hi2, Con{e, t}) == Con{e, t} : List<&2, M.Entry<K, V>>}:
47	  match b:
48	    case True{}:
49	      Empty.absurd({S.outside(~K, ~V, ~cmp, lo2, hi2, Con{e, t}) == Con{e, t} : List<&2, M.Entry<K, V>>}, con_nil(M.Entry<K, V>, e, S.within(~K, ~V, ~cmp, lo2, hi2, t), Equal.trans(List<&2, M.Entry<K, V>>, Con{e, S.within(~K, ~V, ~cmp, lo2, hi2, t)}, S.within(~K, ~V, ~cmp, lo2, hi2, Con{e, t}), Nil{}, Equal.sym(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{e, t}), Con{e, S.within(~K, ~V, ~cmp, lo2, hi2, t)}, VS.w_in(~K, ~V, ~cmp, lo2, hi2, e, t, hb)), h)))
50	    case False{}:
51	      +ht = Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, t), S.within(~K, ~V, ~cmp, lo2, hi2, Con{e, t}), Nil{}, Equal.sym(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{e, t}), S.within(~K, ~V, ~cmp, lo2, hi2, t), VS.w_out(~K, ~V, ~cmp, lo2, hi2, e, t, hb)), h)
52	      Equal.trans(List<&2, M.Entry<K, V>>, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{e, t}), Con{e, S.outside(~K, ~V, ~cmp, lo2, hi2, t)}, Con{e, t}, VS.pk_f(List<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, S.key(K, V, e), lo2, hi2), S.outside(~K, ~V, ~cmp, lo2, hi2, t), Con{e, S.outside(~K, ~V, ~cmp, lo2, hi2, t)}, hb), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, z => Con{e, z}, S.outside(~K, ~V, ~cmp, lo2, hi2, t), t, kf(ht)))
53	
54	def out_id(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +xs: List<&2, M.Entry<K, V>>, +h: {S.within(~K, ~V, ~cmp, lo2, hi2, xs) == Nil{} : List<&2, M.Entry<K, V>>}) -> {S.outside(~K, ~V, ~cmp, lo2, hi2, xs) == xs : List<&2, M.Entry<K, V>>}:
55	  match xs:
56	    case Nil{}:
57	      {==}
58	    case Con{+e, +t}:
59	      oid_c(~K, ~V, ~cmp, lo2, hi2, e, t, h, S.in_range(~K, ~cmp, S.key(K, V, e), lo2, hi2), {==}, ht => out_id(~K, ~V, ~cmp, lo2, hi2, t, ht))
60	
61	def oapp_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +ys: List<&2, M.Entry<K, V>>, +ih: {S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, t, ys)) == SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, t), S.outside(~K, ~V, ~cmp, lo2, hi2, ys)) : List<&2, M.Entry<K, V>>}, +b: Bool, +hb: {S.in_range(~K, ~cmp, S.key(K, V, e), lo2, hi2) == b : Bool}) -> {S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, Con{e, t}, ys)) == SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{e, t}), S.outside(~K, ~V, ~cmp, lo2, hi2, ys)) : List<&2, M.Entry<K, V>>}:
62	  match b:
63	    case True{}:
64	      +l1 = VS.pk_t(List<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, S.key(K, V, e), lo2, hi2), S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, t, ys)), Con{e, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, t, ys))}, hb)
65	      +r1 = VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, z => SC.append(M.Entry<K, V>, z, S.outside(~K, ~V, ~cmp, lo2, hi2, ys)), S.outside(~K, ~V, ~cmp, lo2, hi2, Con{e, t}), S.outside(~K, ~V, ~cmp, lo2, hi2, t), VS.pk_t(List<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, S.key(K, V, e), lo2, hi2), S.outside(~K, ~V, ~cmp, lo2, hi2, t), Con{e, S.outside(~K, ~V, ~cmp, lo2, hi2, t)}, hb))
66	      Equal.trans(List<&2, M.Entry<K, V>>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, Con{e, t}, ys)), SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, t), S.outside(~K, ~V, ~cmp, lo2, hi2, ys)), SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{e, t}), S.outside(~K, ~V, ~cmp, lo2, hi2, ys)), Equal.trans(List<&2, M.Entry<K, V>>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, Con{e, t}, ys)), S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, t, ys)), SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, t), S.outside(~K, ~V, ~cmp, lo2, hi2, ys)), l1, ih), Equal.sym(List<&2, M.Entry<K, V>>, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{e, t}), S.outside(~K, ~V, ~cmp, lo2, hi2, ys)), SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, t), S.outside(~K, ~V, ~cmp, lo2, hi2, ys)), r1))
67	    case False{}:
68	      +l1 = VS.pk_f(List<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, S.key(K, V, e), lo2, hi2), S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, t, ys)), Con{e, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, t, ys))}, hb)
69	      +r1 = VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, z => SC.append(M.Entry<K, V>, z, S.outside(~K, ~V, ~cmp, lo2, hi2, ys)), S.outside(~K, ~V, ~cmp, lo2, hi2, Con{e, t}), Con{e, S.outside(~K, ~V, ~cmp, lo2, hi2, t)}, VS.pk_f(List<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, S.key(K, V, e), lo2, hi2), S.outside(~K, ~V, ~cmp, lo2, hi2, t), Con{e, S.outside(~K, ~V, ~cmp, lo2, hi2, t)}, hb))
70	      Equal.trans(List<&2, M.Entry<K, V>>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, Con{e, t}, ys)), Con{e, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, t), S.outside(~K, ~V, ~cmp, lo2, hi2, ys))}, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{e, t}), S.outside(~K, ~V, ~cmp, lo2, hi2, ys)), Equal.trans(List<&2, M.Entry<K, V>>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, Con{e, t}, ys)), Con{e, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, t, ys))}, Con{e, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, t), S.outside(~K, ~V, ~cmp, lo2, hi2, ys))}, l1, VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, z => Con{e, z}, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, t, ys)), SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, t), S.outside(~K, ~V, ~cmp, lo2, hi2, ys)), ih)), Equal.sym(List<&2, M.Entry<K, V>>, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{e, t}), S.outside(~K, ~V, ~cmp, lo2, hi2, ys)), Con{e, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, t), S.outside(~K, ~V, ~cmp, lo2, hi2, ys))}, r1))
71	
72	def out_app(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +xs: List<&2, M.Entry<K, V>>, +ys: List<&2, M.Entry<K, V>>) -> {S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, xs, ys)) == SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, xs), S.outside(~K, ~V, ~cmp, lo2, hi2, ys)) : List<&2, M.Entry<K, V>>}:
73	  match xs:
74	    case Nil{}:
75	      {==}
76	    case Con{+e, +t}:
77	      oapp_c(~K, ~V, ~cmp, lo2, hi2, e, t, ys, out_app(~K, ~V, ~cmp, lo2, hi2, t, ys), S.in_range(~K, ~cmp, S.key(K, V, e), lo2, hi2), {==})
78	
79	# ---- forward ----
80	
81	
82	# a cursor at the end of the run: its view
83	def cf_end(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +es: List<&2, M.Entry<K, V>>, +cc: Maybe<&2, K>, -sp: S.View<K, V>, -r: M.View<K, V, cmp>, +c2: MI.MCursor<K, V>, +hc2: {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool}, +ec: {S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, True{}} == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor<K, V>}, +hs: {S.VW{S.TM{l, es}, lo2, hi2, False{}} == sp : S.View<K, V>}, +hr: {M.iterator_view(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2)) == r : M.View<K, V, cmp>}) -> VD.VOK(~K, ~V, ~cmp, sp, r):
84	  L.subst(M.View<K, V, cmp>, z => VD.VOK(~K, ~V, ~cmp, sp, z), M.iterator_view(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2)), r, hr, L.subst(S.View<K, V>, z => VD.VOK(~K, ~V, ~cmp, z, M.iterator_view(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2))), S.VW{S.TM{l, es}, lo2, hi2, False{}}, sp, hs, L.subst(S.Cursor<K, V>, z => VD.VOK(~K, ~V, ~cmp, vw_of(K, V, z), M.iterator_view(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2))), CU.cmod(~K, ~V, ~cmp, c2), S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, True{}}, Equal.sym(S.Cursor<K, V>, S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, True{}}, CU.cmod(~K, ~V, ~cmp, c2), ec), iv_ok(~K, ~V, ~cmp, c2, hc2))))
85	
86	
87	def cfn2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +xa: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Nil{})}, None{}, cc, lo2, hi2, True{}} : S.Cursor<K, V>}, +c2: MI.MCursor<K, V>, +ov: Maybe<&2, M.Entry<K, V>>, +h1: {M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)) == (MI.rc(~K, ~V, ~cmp, c2), ov) : M.Cursor<K, V, cmp> & Maybe<&2, M.Entry<K, V>>}, r: {S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)) == (CU.cmod(~K, ~V, ~cmp, c2), ov) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool}) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Nil{}))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))):
88	  match r:
89	    case Tuple{h2, h3}:
90	      +heq = Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, (S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Nil{})}, None{}, cc, lo2, hi2, True{}}, None{}), S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), (CU.cmod(~K, ~V, ~cmp, c2), ov), Equal.sym(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Nil{})}, None{}, cc, lo2, hi2, True{}}, None{}), VS.cong(S.Cursor<K, V>, S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, z => S.iterator_next(~K, ~V, ~cmp, z), CU.cmod(~K, ~V, ~cmp, c), S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Nil{})}, None{}, cc, lo2, hi2, True{}}, hsp)), h2)
91	      +eo = L.pair_snd(S.Cursor<K, V>, Maybe<&2, M.Entry<K, V>>, S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Nil{})}, None{}, cc, lo2, hi2, True{}}, None{}, CU.cmod(~K, ~V, ~cmp, c2), ov, heq)
92	      +ec = L.pair_fst(S.Cursor<K, V>, Maybe<&2, M.Entry<K, V>>, S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Nil{})}, None{}, cc, lo2, hi2, True{}}, None{}, CU.cmod(~K, ~V, ~cmp, c2), ov, heq)
93	      %Equal.sym(M.Cursor<K, V, cmp> & Maybe<&2, M.Entry<K, V>>, M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)), (MI.rc(~K, ~V, ~cmp, c2), ov), h1) : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Nil{}))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), _))
94	      %eo : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Nil{}))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), (MI.rc(~K, ~V, ~cmp, c2), _)))
95	      cf_end(~K, ~V, ~cmp, l, lo2, hi2, SC.append(M.Entry<K, V>, xa, Nil{}), cc, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Nil{}))}, lo2, hi2, False{}}, M.iterator_view(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2)), c2, h3, ec, {==}, {==})
96	
97	def cfn(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +xa: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Nil{})}, None{}, cc, lo2, hi2, True{}} : S.Cursor<K, V>}, p: CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Nil{}))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))):
98	  match p:
99	    case Tuple{+c2, Tuple{+ov, Tuple{+h1, r}}}:
100	      cfn2(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, xa, c, cc, hsp, c2, ov, h1, r)
101	
102	def cfs2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +xa: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, Some{k}, cc, lo2, hi2, True{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})) == True{} : Bool}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == False{} : Bool}, +c2: MI.MCursor<K, V>, +ov: Maybe<&2, M.Entry<K, V>>, +h1: {M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)) == (MI.rc(~K, ~V, ~cmp, c2), ov) : M.Cursor<K, V, cmp> & Maybe<&2, M.Entry<K, V>>}, r: {S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)) == (CU.cmod(~K, ~V, ~cmp, c2), ov) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool}) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))):
103	  match r:
104	    case Tuple{h2, h3}:
105	      +hsv = Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, None{}, cc, lo2, hi2, True{}}, None{})), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, None{}, cc, lo2, hi2, True{}}, None{}), Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, Some{k}, cc, lo2, hi2, True{}}), S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, None{}, cc, lo2, hi2, True{}}, None{})), VS.cong(S.Cursor<K, V>, S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, z => S.iterator_next(~K, ~V, ~cmp, z), CU.cmod(~K, ~V, ~cmp, c), S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, Some{k}, cc, lo2, hi2, True{}}, hsp), VZ.sp_f(~K, ~V, ~cmp, ~o, l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), xa, k, v, t, {==}, hord, cc, lo2, hi2)), VS.pk_f(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, None{}, cc, lo2, hi2, True{}}, None{}), hb))
106	      +heq = Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, (S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, None{}, cc, lo2, hi2, True{}}, None{}), S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), (CU.cmod(~K, ~V, ~cmp, c2), ov), Equal.sym(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, None{}, cc, lo2, hi2, True{}}, None{}), hsv), h2)
107	      +eo = L.pair_snd(S.Cursor<K, V>, Maybe<&2, M.Entry<K, V>>, S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, None{}, cc, lo2, hi2, True{}}, None{}, CU.cmod(~K, ~V, ~cmp, c2), ov, heq)
108	      +ec = L.pair_fst(S.Cursor<K, V>, Maybe<&2, M.Entry<K, V>>, S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, None{}, cc, lo2, hi2, True{}}, None{}, CU.cmod(~K, ~V, ~cmp, c2), ov, heq)
109	      +hbu = VS.bu_of(~K, ~cmp, lo2, hi2, k, L.and_left(S.above_lower(~K, ~cmp, k, lo2), VS.allal(~K, ~V, ~cmp, lo2, t), hal), hb)
110	      +ho = OR.ord_app_r(~K, ~V, ~cmp, xa, Con{M.Entry{k, v}, t}, hord)
111	      +hw = Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}), S.within(~K, ~V, ~cmp, lo2, hi2, t), Nil{}, VS.w_out(~K, ~V, ~cmp, lo2, hi2, M.Entry{k, v}, t, hb), VS.wnil(~K, ~V, ~cmp, ~o, lo2, hi2, k, t, hbu, OR.ord_gt(~K, ~V, ~cmp, ~o, t, M.Entry{k, v}, ho)))
112	      +hs = VS.cong(List<&2, M.Entry<K, V>>, S.View<K, V>, z => S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, z)}, lo2, hi2, False{}}, Con{M.Entry{k, v}, t}, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}), Equal.sym(List<&2, M.Entry<K, V>>, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}), Con{M.Entry{k, v}, t}, out_id(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}, hw)))
113	      %Equal.sym(M.Cursor<K, V, cmp> & Maybe<&2, M.Entry<K, V>>, M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)), (MI.rc(~K, ~V, ~cmp, c2), ov), h1) : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), _))
114	      %eo : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), (MI.rc(~K, ~V, ~cmp, c2), _)))
115	      cf_end(~K, ~V, ~cmp, l, lo2, hi2, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), cc, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}))}, lo2, hi2, False{}}, M.iterator_view(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2)), c2, h3, ec, hs, {==})
116	
117	def cfs(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +xa: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, Some{k}, cc, lo2, hi2, True{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})) == True{} : Bool}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == False{} : Bool}, p: CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))):
118	  match p:
119	    case Tuple{+c2, Tuple{+ov, Tuple{+h1, r}}}:
120	      cfs2(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, xa, k, v, t, c, cc, hsp, hord, hal, hb, c2, ov, h1, r)
121	
122	def cft4(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +xa: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, Some{k}, cc, lo2, hi2, True{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})) == True{} : Bool}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == True{} : Bool}, +c2: MI.MCursor<K, V>, +ec: {S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}} == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor<K, V>}, +c3: MI.MCursor<K, V>, +o3: Maybe<&2, V>, +g1: {M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2)) == (MI.rc(~K, ~V, ~cmp, c3), o3) : M.Cursor<K, V, cmp> & Maybe<&2, V>}, r: {S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c2)) == (CU.cmod(~K, ~V, ~cmp, c3), o3) : S.Cursor<K, V> & Maybe<&2, V>} & {CU.cgood(~K, ~V, ~cmp, c3) == True{} : Bool}, kont: @+kc3: MI.MCursor<K, V> -> @+kh3: {CU.cgood(~K, ~V, ~cmp, kc3) == True{} : Bool} -> @+ks3: {CU.cmod(~K, ~V, ~cmp, kc3) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, t)}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), None{}, lo2, hi2, True{}} : S.Cursor<K, V>} -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.appen
123	  match r:
124	    case Tuple{g2, g3}:
125	      +f1 = VS.cong(S.Cursor<K, V>, S.Cursor<K, V> & Maybe<&2, V>, z => S.iterator_remove(~K, ~V, ~cmp, z), CU.cmod(~K, ~V, ~cmp, c2), S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Equal.sym(S.Cursor<K, V>, S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, CU.cmod(~K, ~V, ~cmp, c2), ec))
126	      +heq = Equal.trans(S.Cursor<K, V> & Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}), S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c2)), (CU.cmod(~K, ~V, ~cmp, c3), o3), Equal.sym(S.Cursor<K, V> & Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c2)), S.iterator_remove(~K, ~V, ~cmp, S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}), f1), g2)
127	      +ec3 = L.pair_fst(S.Cursor<K, V>, Maybe<&2, V>, S.CR{S.TM{l, S.del(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}))}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), None{}, lo2, hi2, True{}}, S.find(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})), CU.cmod(~K, ~V, ~cmp, c3), o3, heq)
128	      +hdel = DO.del_mid(~K, ~V, ~cmp, ~o, k, xa, M.Entry{k, v}, t, OR.ord_mid_l(~K, ~V, ~cmp, ~o, xa, M.Entry{k, v}, t, hord), O.refl(~K, ~cmp, ~o, k))
129	      +hsp3 = Equal.trans(S.Cursor<K, V>, CU.cmod(~K, ~V, ~cmp, c3), S.CR{S.TM{l, S.del(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}))}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), None{}, lo2, hi2, True{}}, S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, t)}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), None{}, lo2, hi2, True{}}, Equal.sym(S.Cursor<K, V>, S.CR{S.TM{l, S.del(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}))}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), None{}, lo2, hi2, True{}}, CU.cmod(~K, ~V, ~cmp, c3), ec3), VS.cong(List<&2, M.Entry<K, V>>, S.Cursor<K, V>, z => S.CR{S.TM{l, z}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), None{}, lo2, hi2, True{}}, S.del(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})), SC.append(M.Entry<K, V>, xa, t), hdel))
130	      %Equal.sym(M.Cursor<K, V, cmp> & Maybe<&2, V>, M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2)), (MI.rc(~K, ~V, ~cmp, c3), o3), g1) : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), M.view_clear_next(~K, ~V, ~cmp, _)))
131	      +eo = VS.cong(List<&2, M.Entry<K, V>>, S.View<K, V>, z => S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, z)}, lo2, hi2, False{}}, S.outside(~K, ~V, ~cmp, lo2, hi2, t), S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}), Equal.sym(List<&2, M.Entry<K, V>>, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}), S.outside(~K, ~V, ~cmp, lo2, hi2, t), VS.pk_t(List<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), S.outside(~K, ~V, ~cmp, lo2, hi2, t), Con{M.Entry{k, v}, S.outside(~K, ~V, ~cmp, lo2, hi2, t)}, hb)))
132	      L.subst(S.View<K, V>, z => VD.VOK(~K, ~V, ~cmp, z, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c3)))), S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, t))}, lo2, hi2, False{}}, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}))}, lo2, hi2, False{}}, eo, kont(c3, g3, hsp3))
133	
134	def cft3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +xa: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, Some{k}, cc, lo2, hi2, True{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})) == True{} : Bool}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == True{} : Bool}, +c2: MI.MCursor<K, V>, +ec: {S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}} == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor<K, V>}, q: CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c2)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2))), kont: @+kc3: MI.MCursor<K, V> -> @+kh3: {CU.cgood(~K, ~V, ~cmp, kc3) == True{} : Bool} -> @+ks3: {CU.cmod(~K, ~V, ~cmp, kc3) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, t)}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), None{}, lo2, hi2, True{}} : S.Cursor<K, V>} -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, t))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V
135	  match q:
136	    case Tuple{+c3, Tuple{+o3, Tuple{+g1, r}}}:
137	      cft4(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, xa, k, v, t, c, cc, hsp, hord, hal, hb, c2, ec, c3, o3, g1, r, kont)
138	
139	def cft2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +xa: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, Some{k}, cc, lo2, hi2, True{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})) == True{} : Bool}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == True{} : Bool}, +c2: MI.MCursor<K, V>, +ov: Maybe<&2, M.Entry<K, V>>, +h1: {M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)) == (MI.rc(~K, ~V, ~cmp, c2), ov) : M.Cursor<K, V, cmp> & Maybe<&2, M.Entry<K, V>>}, r: {S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)) == (CU.cmod(~K, ~V, ~cmp, c2), ov) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool}, kont: @+kc3: MI.MCursor<K, V> -> @+kh3: {CU.cgood(~K, ~V, ~cmp, kc3) == True{} : Bool} -> @+ks3: {CU.cmod(~K, ~V, ~cmp, kc3) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, t)}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), None{}, lo2, hi2, True{}} : S.Cursor<K, V>} -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, t))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), M.iterator_next(~K, ~V, ~
140	  match r:
141	    case Tuple{h2, h3}:
142	      +hsv = Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, None{}, cc, lo2, hi2, True{}}, None{})), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, Some{k}, cc, lo2, hi2, True{}}), S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, None{}, cc, lo2, hi2, True{}}, None{})), VS.cong(S.Cursor<K, V>, S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, z => S.iterator_next(~K, ~V, ~cmp, z), CU.cmod(~K, ~V, ~cmp, c), S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, Some{k}, cc, lo2, hi2, True{}}, hsp), VZ.sp_f(~K, ~V, ~cmp, ~o, l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), xa, k, v, t, {==}, hord, cc, lo2, hi2)), VS.pk_t(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, None{}, cc, lo2, hi2, True{}}, None{}), hb))
143	      +heq = Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, (S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), (CU.cmod(~K, ~V, ~cmp, c2), ov), Equal.sym(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), hsv), h2)
144	      +eo = L.pair_snd(S.Cursor<K, V>, Maybe<&2, M.Entry<K, V>>, S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}, CU.cmod(~K, ~V, ~cmp, c2), ov, heq)
145	      +ec = L.pair_fst(S.Cursor<K, V>, Maybe<&2, M.Entry<K, V>>, S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}, CU.cmod(~K, ~V, ~cmp, c2), ov, heq)
146	      %Equal.sym(M.Cursor<K, V, cmp> & Maybe<&2, M.Entry<K, V>>, M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)), (MI.rc(~K, ~V, ~cmp, c2), ov), h1) : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), _))
147	      %eo : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), (MI.rc(~K, ~V, ~cmp, c2), _)))
148	      cft3(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, xa, k, v, t, c, cc, hsp, hord, hal, hb, c2, ec, rok(c2, h3), kont)
149	
150	def cft(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +xa: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, Some{k}, cc, lo2, hi2, True{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})) == True{} : Bool}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == True{} : Bool}, p: CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c))), kont: @+kc3: MI.MCursor<K, V> -> @+kh3: {CU.cgood(~K, ~V, ~cmp, kc3) == True{} : Bool} -> @+ks3: {CU.cmod(~K, ~V, ~cmp, kc3) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, t)}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), None{}, lo2, hi2, True{}} : S.Cursor<K, V>} -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, t))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, kc3))))) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(S
151	  match p:
152	    case Tuple{+c2, Tuple{+ov, Tuple{+h1, r}}}:
153	      cft2(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, xa, k, v, t, c, cc, hsp, hord, hal, hb, c2, ov, h1, r, kont)
154	
155	def cfc(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +xa: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})}, Some{k}, cc, lo2, hi2, True{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t})) == True{} : Bool}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +b: Bool, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == b : Bool}, p: CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c))), kont: @+kc3: MI.MCursor<K, V> -> @+kh3: {CU.cgood(~K, ~V, ~cmp, kc3) == True{} : Bool} -> @+ks3: {CU.cmod(~K, ~V, ~cmp, kc3) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, t)}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), None{}, lo2, hi2, True{}} : S.Cursor<K, V>} -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, t))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, kc3))))) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.
156	  match b:
157	    case True{}:
158	      cft(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, xa, k, v, t, c, cc, hsp, hord, hal, hb, p, kont)
159	    case False{}:
160	      cfs(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, xa, k, v, t, c, cc, hsp, hord, hal, hb, p)
161	
162	# the clear forward: every entry of the run from the cursor on removed
163	def clf(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +xa: List<&2, M.Entry<K, V>>, +bs: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, bs)}, S.key_m(K, V, S.head(M.Entry<K, V>, bs)), cc, lo2, hi2, True{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, xa, bs)) == True{} : Bool}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, bs) == True{} : Bool}) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, bs))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, bs), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))):
164	  match bs:
165	    case Nil{}:
166	      cfn(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, xa, c, cc, hsp, nok(c, hc))
167	    case Con{M.Entry{+k, +v}, +t}:
168	      cfc(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, xa, k, v, t, c, cc, hsp, hord, hal, S.in_range(~K, ~cmp, k, lo2, hi2), {==}, nok(c, hc), kc3 => kh3 => ks3 => clf(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, xa, t, kc3, None{}, kh3, ks3, DO.ord_drop(~K, ~V, ~cmp, ~o, xa, M.Entry{k, v}, t, hord), L.and_right(S.above_lower(~K, ~cmp, k, lo2), VS.allal(~K, ~V, ~cmp, lo2, t), hal)))
169	
170	# ---- backward: the entries before the cursor, reversed, then the rest ----
171	
172	
173	def cb_end(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +es: List<&2, M.Entry<K, V>>, +cc: Maybe<&2, K>, -sp: S.View<K, V>, -r: M.View<K, V, cmp>, +c2: MI.MCursor<K, V>, +hc2: {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool}, +ec: {S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, False{}} == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor<K, V>}, +hs: {S.VW{S.TM{l, es}, lo2, hi2, True{}} == sp : S.View<K, V>}, +hr: {M.iterator_view(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2)) == r : M.View<K, V, cmp>}) -> VD.VOK(~K, ~V, ~cmp, sp, r):
174	  L.subst(M.View<K, V, cmp>, z => VD.VOK(~K, ~V, ~cmp, sp, z), M.iterator_view(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2)), r, hr, L.subst(S.View<K, V>, z => VD.VOK(~K, ~V, ~cmp, z, M.iterator_view(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2))), S.VW{S.TM{l, es}, lo2, hi2, True{}}, sp, hs, L.subst(S.Cursor<K, V>, z => VD.VOK(~K, ~V, ~cmp, vw_of(K, V, z), M.iterator_view(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2))), CU.cmod(~K, ~V, ~cmp, c2), S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, False{}}, Equal.sym(S.Cursor<K, V>, S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, False{}}, CU.cmod(~K, ~V, ~cmp, c2), ec), iv_ok(~K, ~V, ~cmp, c2, hc2))))
175	
176	def cbn2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +bs: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, Nil{}), bs)}, None{}, cc, lo2, hi2, False{}} : S.Cursor<K, V>}, +c2: MI.MCursor<K, V>, +ov: Maybe<&2, M.Entry<K, V>>, +h1: {M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)) == (MI.rc(~K, ~V, ~cmp, c2), ov) : M.Cursor<K, V, cmp> & Maybe<&2, M.Entry<K, V>>}, r: {S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)) == (CU.cmod(~K, ~V, ~cmp, c2), ov) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool}) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Nil{})), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))):
177	  match r:
178	    case Tuple{h2, h3}:
179	      +heq = Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, (S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, Nil{}), bs)}, None{}, cc, lo2, hi2, False{}}, None{}), S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), (CU.cmod(~K, ~V, ~cmp, c2), ov), Equal.sym(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, Nil{}), bs)}, None{}, cc, lo2, hi2, False{}}, None{}), VS.cong(S.Cursor<K, V>, S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, z => S.iterator_next(~K, ~V, ~cmp, z), CU.cmod(~K, ~V, ~cmp, c), S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, Nil{}), bs)}, None{}, cc, lo2, hi2, False{}}, hsp)), h2)
180	      +eo = L.pair_snd(S.Cursor<K, V>, Maybe<&2, M.Entry<K, V>>, S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, Nil{}), bs)}, None{}, cc, lo2, hi2, False{}}, None{}, CU.cmod(~K, ~V, ~cmp, c2), ov, heq)
181	      +ec = L.pair_fst(S.Cursor<K, V>, Maybe<&2, M.Entry<K, V>>, S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, Nil{}), bs)}, None{}, cc, lo2, hi2, False{}}, None{}, CU.cmod(~K, ~V, ~cmp, c2), ov, heq)
182	      %Equal.sym(M.Cursor<K, V, cmp> & Maybe<&2, M.Entry<K, V>>, M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)), (MI.rc(~K, ~V, ~cmp, c2), ov), h1) : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Nil{})), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), _))
183	      %eo : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Nil{})), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), (MI.rc(~K, ~V, ~cmp, c2), _)))
184	      cb_end(~K, ~V, ~cmp, l, lo2, hi2, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, Nil{}), bs), cc, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Nil{})), bs)}, lo2, hi2, True{}}, M.iterator_view(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2)), c2, h3, ec, {==}, {==})
185	
186	def cbn(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +bs: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, Nil{}), bs)}, None{}, cc, lo2, hi2, False{}} : S.Cursor<K, V>}, p: CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Nil{})), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))):
187	  match p:
188	    case Tuple{+c2, Tuple{+ov, Tuple{+h1, r}}}:
189	      cbn2(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, bs, c, cc, hsp, c2, ov, h1, r)
190	
191	def cbs2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +bs: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, Some{k}, cc, lo2, hi2, False{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)) == True{} : Bool}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == False{} : Bool}, +c2: MI.MCursor<K, V>, +ov: Maybe<&2, M.Entry<K, V>>, +h1: {M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)) == (MI.rc(~K, ~V, ~cmp, c2), ov) : M.Cursor<K, V, cmp> & Maybe<&2, M.Entry<K, V>>}, r: {S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)) == (CU.cmod(~K, ~V, ~cmp, c2), ov) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool}) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t})), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))):
192	  match r:
193	    case Tuple{h2, h3}:
194	      +hsv = Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, None{}, cc, lo2, hi2, False{}}, None{})), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, None{}, cc, lo2, hi2, False{}}, None{}), Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, Some{k}, cc, lo2, hi2, False{}}), S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, None{}, cc, lo2, hi2, False{}}, None{})), VS.cong(S.Cursor<K, V>, S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, z => S.iterator_next(~K, ~V, ~cmp, z), CU.cmod(~K, ~V, ~cmp, c), S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, Some{k}, cc, lo2, hi2, False{}}, hsp), VZ.sp_b(~K, ~V, ~cmp, ~o, l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs), SC.reverse(M.Entry<K, V>, t), k, v, bs, LL.snoc_append_cons(M.Entry<K, 
195	      +heq = Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, (S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, None{}, cc, lo2, hi2, False{}}, None{}), S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), (CU.cmod(~K, ~V, ~cmp, c2), ov), Equal.sym(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, None{}, cc, lo2, hi2, False{}}, None{}), hsv), h2)
196	      +eo = L.pair_snd(S.Cursor<K, V>, Maybe<&2, M.Entry<K, V>>, S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, None{}, cc, lo2, hi2, False{}}, None{}, CU.cmod(~K, ~V, ~cmp, c2), ov, heq)
197	      +ec = L.pair_fst(S.Cursor<K, V>, Maybe<&2, M.Entry<K, V>>, S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, None{}, cc, lo2, hi2, False{}}, None{}, CU.cmod(~K, ~V, ~cmp, c2), ov, heq)
198	      +hal = VS.al_of(~K, ~cmp, lo2, hi2, k, L.and_left(S.below_upper(~K, ~cmp, k, hi2), VS.allbu(~K, ~V, ~cmp, hi2, t), hbu), hb)
199	      +hw1 = VS.wnil_lt(~K, ~V, ~cmp, ~o, lo2, hi2, k, SC.reverse(M.Entry<K, V>, t), hal, OR.ord_mid_l(~K, ~V, ~cmp, ~o, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}, bs, L.subst(List<&2, M.Entry<K, V>>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs), SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, bs}), LL.snoc_append_cons(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}, bs), hord)))
200	      +hw = Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, Nil{}})), Nil{}, VZ.wl_snoc(~K, ~V, ~cmp, lo2, hi2, t, k, v), L.subst(List<&2, M.Entry<K, V>>, q => {SC.append(M.Entry<K, V>, q, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, Nil{}})) == Nil{} : List<&2, M.Entry<K, V>>}, Nil{}, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), Equal.sym(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), Nil{}, hw1), VS.w_out(~K, ~V, ~cmp, lo2, hi2, M.Entry{k, v}, Nil{}, hb)))
201	      +hs = VS.cong(List<&2, M.Entry<K, V>>, S.View<K, V>, z => S.VW{S.TM{l, SC.append(M.Entry<K, V>, z, bs)}, lo2, hi2, True{}}, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), S.outside(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), Equal.sym(List<&2, M.Entry<K, V>>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), out_id(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), hw)))
202	      %Equal.sym(M.Cursor<K, V, cmp> & Maybe<&2, M.Entry<K, V>>, M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)), (MI.rc(~K, ~V, ~cmp, c2), ov), h1) : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t})), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), _))
203	      %eo : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t})), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), (MI.rc(~K, ~V, ~cmp, c2), _)))
204	      cb_end(~K, ~V, ~cmp, l, lo2, hi2, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs), cc, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t})), bs)}, lo2, hi2, True{}}, M.iterator_view(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2)), c2, h3, ec, hs, {==})
205	
206	def cbs(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +bs: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, Some{k}, cc, lo2, hi2, False{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)) == True{} : Bool}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == False{} : Bool}, p: CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t})), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))):
207	  match p:
208	    case Tuple{+c2, Tuple{+ov, Tuple{+h1, r}}}:
209	      cbs2(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, bs, k, v, t, c, cc, hsp, hord, hbu, hb, c2, ov, h1, r)
210	
211	def cbt4(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +bs: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, Some{k}, cc, lo2, hi2, False{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)) == True{} : Bool}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == True{} : Bool}, +c2: MI.MCursor<K, V>, +ec: {S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}} == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor<K, V>}, +c3: MI.MCursor<K, V>, +o3: Maybe<&2, V>, +g1: {M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2)) == (MI.rc(~K, ~V, ~cmp, c3), o3) : M.Cursor<K, V, cmp> & Maybe<&2, V>}, r: {S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c2)) == (CU.cmod(~K, ~V, ~cmp, c3), o3) : S.Cursor<K, V> & Maybe<&2, V>} & {CU.cgood(~K, ~V, ~cmp, c3) == True{} : Bool}, kont: @+kc3: MI.MCursor<K, V> -> @+kh3: {CU.cgood(~K, ~V, ~cmp, kc3) == True{} : Bool} -> @+ks3: {CU.cmod(~K, ~V, ~cmp, kc3) == S.CR{S.TM{
212	  match r:
213	    case Tuple{g2, g3}:
214	      +f1 = VS.cong(S.Cursor<K, V>, S.Cursor<K, V> & Maybe<&2, V>, z => S.iterator_remove(~K, ~V, ~cmp, z), CU.cmod(~K, ~V, ~cmp, c2), S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}, Equal.sym(S.Cursor<K, V>, S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}, CU.cmod(~K, ~V, ~cmp, c2), ec))
215	      +heq = Equal.trans(S.Cursor<K, V> & Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}), S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c2)), (CU.cmod(~K, ~V, ~cmp, c3), o3), Equal.sym(S.Cursor<K, V> & Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c2)), S.iterator_remove(~K, ~V, ~cmp, S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}), f1), g2)
216	      +ec3 = L.pair_fst(S.Cursor<K, V>, Maybe<&2, V>, S.CR{S.TM{l, S.del(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs))}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), None{}, lo2, hi2, False{}}, S.find(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)), CU.cmod(~K, ~V, ~cmp, c3), o3, heq)
217	      +hdel = Equal.trans(List<&2, M.Entry<K, V>>, S.del(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)), S.del(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, bs})), SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), bs), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, z => S.del(~K, ~V, ~cmp, k, z), SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs), SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, bs}), LL.snoc_append_cons(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}, bs)), DO.del_mid(~K, ~V, ~cmp, ~o, k, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}, bs, OR.ord_mid_l(~K, ~V, ~cmp, ~o, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}, bs, L.subst(List<&2, M.Entry<K, V>>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs), SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, bs}), LL.snoc_append_cons(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}, bs), hord)), O.refl(~K, ~cmp, ~o, k)))
218	      +hsp3 = Equal.trans(S.Cursor<K, V>, CU.cmod(~K, ~V, ~cmp, c3), S.CR{S.TM{l, S.del(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs))}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), None{}, lo2, hi2, False{}}, S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), None{}, lo2, hi2, False{}}, Equal.sym(S.Cursor<K, V>, S.CR{S.TM{l, S.del(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs))}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), None{}, lo2, hi2, False{}}, CU.cmod(~K, ~V, ~cmp, c3), ec3), VS.cong(List<&2, M.Entry<K, V>>, S.Cursor<K, V>, z => S.CR{S.TM{l, z}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), None{}, lo2, hi2, False{}}, S.del(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)), SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), bs), hdel))
219	      %Equal.sym(M.Cursor<K, V, cmp> & Maybe<&2, V>, M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2)), (MI.rc(~K, ~V, ~cmp, c3), o3), g1) : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t})), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), M.view_clear_next(~K, ~V, ~cmp, _)))
220	      +eo1 = Equal.trans(List<&2, M.Entry<K, V>>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, Nil{}})), SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, Nil{}})), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, z => S.outside(~K, ~V, ~cmp, lo2, hi2, z), SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, Nil{}}), LL.snoc_append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), out_app(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, Nil{}}))
221	      +eo2 = Equal.trans(List<&2, M.Entry<K, V>>, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, Nil{}})), SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), Nil{}), S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, z => SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), z), S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, Nil{}}), Nil{}, VS.pk_t(List<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), Nil{}, Con{M.Entry{k, v}, Nil{}}, hb)), LL.append_nil(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))))
222	      +eo = VS.cong(List<&2, M.Entry<K, V>>, S.View<K, V>, z => S.VW{S.TM{l, SC.append(M.Entry<K, V>, z, bs)}, lo2, hi2, True{}}, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), S.outside(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), Equal.sym(List<&2, M.Entry<K, V>>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), Equal.trans(List<&2, M.Entry<K, V>>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), S.outside(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, Nil{}})), S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), eo1, eo2)))
223	      L.subst(S.View<K, V>, z => VD.VOK(~K, ~V, ~cmp, z, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c3)))), S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), bs)}, lo2, hi2, True{}}, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t})), bs)}, lo2, hi2, True{}}, eo, kont(c3, g3, hsp3))
224	
225	def cbt3(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +bs: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, Some{k}, cc, lo2, hi2, False{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)) == True{} : Bool}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == True{} : Bool}, +c2: MI.MCursor<K, V>, +ec: {S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}} == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor<K, V>}, q: CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c2)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2))), kont: @+kc3: MI.MCursor<K, V> -> @+kh3: {CU.cgood(~K, ~V, ~cmp, kc3) == True{} : Bool} -> @+ks3: {CU.cmod(~K, ~V, ~cmp, kc3) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), None{}, lo2, hi2, False{}} : S.Cursor<K, V>} -> VD.VOK(~K, ~V, ~cmp
226	  match q:
227	    case Tuple{+c3, Tuple{+o3, Tuple{+g1, r}}}:
228	      cbt4(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, bs, k, v, t, c, cc, hsp, hord, hbu, hb, c2, ec, c3, o3, g1, r, kont)
229	
230	def cbt2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +bs: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, Some{k}, cc, lo2, hi2, False{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)) == True{} : Bool}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == True{} : Bool}, +c2: MI.MCursor<K, V>, +ov: Maybe<&2, M.Entry<K, V>>, +h1: {M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)) == (MI.rc(~K, ~V, ~cmp, c2), ov) : M.Cursor<K, V, cmp> & Maybe<&2, M.Entry<K, V>>}, r: {S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)) == (CU.cmod(~K, ~V, ~cmp, c2), ov) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool}, kont: @+kc3: MI.MCursor<K, V> -> @+kh3: {CU.cgood(~K, ~V, ~cmp, kc3) == True{} : Bool} -> @+ks3: {CU.cmod(~K, ~V, ~cmp, kc3) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), None{}, lo2, hi2, False{}} : S.Cursor<K, V>} -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V,
231	  match r:
232	    case Tuple{h2, h3}:
233	      +hsv = Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, None{}, cc, lo2, hi2, False{}}, None{})), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, Some{k}, cc, lo2, hi2, False{}}), S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, None{}, cc, lo2, hi2, False{}}, None{})), VS.cong(S.Cursor<K, V>, S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, z => S.iterator_next(~K, ~V, ~cmp, z), CU.cmod(~K, ~V, ~cmp, c), S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, Some{k}, cc, lo2, hi2, False{}}, hsp), VZ.sp_b(~K, ~V, ~cmp, ~o, l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})
234	      +heq = Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, (S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), (CU.cmod(~K, ~V, ~cmp, c2), ov), Equal.sym(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), (S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), hsv), h2)
235	      +eo = L.pair_snd(S.Cursor<K, V>, Maybe<&2, M.Entry<K, V>>, S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}, CU.cmod(~K, ~V, ~cmp, c2), ov, heq)
236	      +ec = L.pair_fst(S.Cursor<K, V>, Maybe<&2, M.Entry<K, V>>, S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}, CU.cmod(~K, ~V, ~cmp, c2), ov, heq)
237	      %Equal.sym(M.Cursor<K, V, cmp> & Maybe<&2, M.Entry<K, V>>, M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)), (MI.rc(~K, ~V, ~cmp, c2), ov), h1) : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t})), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), _))
238	      %eo : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t})), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), (MI.rc(~K, ~V, ~cmp, c2), _)))
239	      cbt3(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, bs, k, v, t, c, cc, hsp, hord, hbu, hb, c2, ec, rok(c2, h3), kont)
240	
241	def cbt(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +bs: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, Some{k}, cc, lo2, hi2, False{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)) == True{} : Bool}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == True{} : Bool}, p: CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c))), kont: @+kc3: MI.MCursor<K, V> -> @+kh3: {CU.cgood(~K, ~V, ~cmp, kc3) == True{} : Bool} -> @+ks3: {CU.cmod(~K, ~V, ~cmp, kc3) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), None{}, lo2, hi2, False{}} : S.Cursor<K, V>} -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, kc3))))) -> VD.VOK(~K, ~V
242	  match p:
243	    case Tuple{+c2, Tuple{+ov, Tuple{+h1, r}}}:
244	      cbt2(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, bs, k, v, t, c, cc, hsp, hord, hbu, hb, c2, ov, h1, r, kont)
245	
246	def cbc(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +bs: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, Some{k}, cc, lo2, hi2, False{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)) == True{} : Bool}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +b: Bool, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == b : Bool}, p: CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c))), kont: @+kc3: MI.MCursor<K, V> -> @+kh3: {CU.cgood(~K, ~V, ~cmp, kc3) == True{} : Bool} -> @+ks3: {CU.cmod(~K, ~V, ~cmp, kc3) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), None{}, lo2, hi2, False{}} : S.Cursor<K, V>} -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, kc3))))) -> VD.VOK(~
247	  match b:
248	    case True{}:
249	      cbt(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, bs, k, v, t, c, cc, hsp, hord, hbu, hb, p, kont)
250	    case False{}:
251	      cbs(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, bs, k, v, t, c, cc, hsp, hord, hbu, hb, p)
252	
253	
254	# the clear backward: every entry of the run before the cursor removed
255	def clb(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~nok: @+nc: MI.MCursor<K, V> -> @+nh: {CU.cgood(~K, ~V, ~cmp, nc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, nc)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, nc))), ~rok: @+rc: MI.MCursor<K, V> -> @+rh: {CU.cgood(~K, ~V, ~cmp, rc) == True{} : Bool} -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, rc)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, rc))), +l: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +bs: List<&2, M.Entry<K, V>>, +rr: List<&2, M.Entry<K, V>>, +c: MI.MCursor<K, V>, +cc: Maybe<&2, K>, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}, +hsp: {CU.cmod(~K, ~V, ~cmp, c) == S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, rr), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, rr))), cc, lo2, hi2, False{}} : S.Cursor<K, V>}, +hord: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, rr), bs)) == True{} : Bool}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, rr) == True{} : Bool}) -> VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, rr)), bs)}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, rr), x), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)))):
256	  match rr:
257	    case Nil{}:
258	      cbn(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, bs, c, cc, hsp, nok(c, hc))
259	    case Con{M.Entry{+k, +v}, +t}:
260	      cbc(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, bs, k, v, t, c, cc, Equal.trans(S.Cursor<K, V>, CU.cmod(~K, ~V, ~cmp, c), S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), cc, lo2, hi2, False{}}, S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, Some{k}, cc, lo2, hi2, False{}}, hsp, VS.cong(Maybe<&2, M.Entry<K, V>>, S.Cursor<K, V>, z => S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs)}, S.key_m(K, V, z), cc, lo2, hi2, False{}}, S.last(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), Some{M.Entry{k, v}}, LL.last_snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), hord, hbu, S.in_range(~K, ~cmp, k, lo2, hi2), {==}, nok(c, hc), kc3 => kh3 => ks3 => clb(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, bs, t, kc3, None{}, kh3, ks3, DO.ord_drop(~K, ~V, ~cmp, ~o, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}, bs, L.subst(List<&2, M.Entry<K, V>>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs), SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, bs}), LL.snoc_append_cons(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}, bs), hord)), L.and_right(S.below_upper(~K, ~cmp, k, hi2), VS.allbu(~K, ~V, ~cmp, hi2, t), hbu)))