import Base
import ../../lib/logic.bend as L
import ../../lib/list.bend as LL
import ../../lib/order.bend as O
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/balanced_search_tree/main.bend as S
import ../../../src/containers/balanced_search_tree.bend as M
import ./state.bend as ST
import ./mirror.bend as MI
import ./ord.bend as OR
import ./dord.bend as DO
import ./cur.bend as CU
import ./vsp.bend as VS
import ./vsz.bend as VZ
import ./vdef.bend as VD

# A view's clear: the implementation walks the view's cursor, removing each
# entry in range, until one is out of range; each step is the specification
# cursor's, so what is left is the entries outside the view.
# (source: tools/generators/tm_hand/vclr.src)


# ---- the cursor's view ----

def vw_of(-K: Data, -V: Data, c: S.Cursor<K, V>) -> S.View<K, V>:
  match c:
    case S.CR{m, nx, cu, lo, hi, fw}:
      S.VW{m, lo, hi, Bool.not(fw)}

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))):
  match c2:
    case MI.MC{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +a, +b, +lo3, +hi3, +fw3}:
      (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))))

def is_nil(-A: Data, xs: List<&2, A>) -> Bool:
  match xs:
    case Nil{}:
      True{}
    case Con{h, t}:
      False{}

def con_nil(-A: Data, +x: A, +t: List<&2, A>, +h: {Con{x, t} == Nil{} : List<&2, A>}) -> Empty:
  L.false_true(VS.cong(List<&2, A>, Bool, z => is_nil(A, z), Con{x, t}, Nil{}, h))

# nothing within: nothing to clear
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>>}:
  match b:
    case True{}:
      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)))
    case False{}:
      +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)
      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)))

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>>}:
  match xs:
    case Nil{}:
      {==}
    case Con{+e, +t}:
      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))

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>>}:
  match b:
    case True{}:
      +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)
      +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))
      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))
    case False{}:
      +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)
      +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))
      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))

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>>}:
  match xs:
    case Nil{}:
      {==}
    case Con{+e, +t}:
      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), {==})

# ---- forward ----


# a cursor at the end of the run: its view
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):
  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))))


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)))):
  match r:
    case Tuple{h2, h3}:
      +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)
      +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)
      +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)
      %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), _))
      %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), _)))
      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, {==}, {==})

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)))):
  match p:
    case Tuple{+c2, Tuple{+ov, Tuple{+h1, r}}}:
      cfn2(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, xa, c, cc, hsp, c2, ov, h1, r)

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)))):
  match r:
    case Tuple{h2, h3}:
      +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))
      +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)
      +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)
      +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)
      +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)
      +ho = OR.ord_app_r(~K, ~V, ~cmp, xa, Con{M.Entry{k, v}, t}, hord)
      +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)))
      +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)))
      %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), _))
      %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), _)))
      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, {==})

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)))):
  match p:
    case Tuple{+c2, Tuple{+ov, Tuple{+h1, r}}}:
      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)

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.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(SC.length(M.Entry<K, V>, t), x), M.view_clear_next(~K, ~V, ~cmp, M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2))))):
  match r:
    case Tuple{g2, g3}:
      +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))
      +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)
      +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)
      +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))
      +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))
      %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, _)))
      +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)))
      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))

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, ~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(SC.length(M.Entry<K, V>, t), x), M.view_clear_next(~K, ~V, ~cmp, M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2))))):
  match q:
    case Tuple{+c3, Tuple{+o3, Tuple{+g1, r}}}:
      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)

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, ~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(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)))):
  match r:
    case Tuple{h2, h3}:
      +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))
      +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)
      +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)
      +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)
      %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), _))
      %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), _)))
      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)

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(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)))):
  match p:
    case Tuple{+c2, Tuple{+ov, Tuple{+h1, r}}}:
      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)

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.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)))):
  match b:
    case True{}:
      cft(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, xa, k, v, t, c, cc, hsp, hord, hal, hb, p, kont)
    case False{}:
      cfs(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, xa, k, v, t, c, cc, hsp, hord, hal, hb, p)

# the clear forward: every entry of the run from the cursor on removed
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)))):
  match bs:
    case Nil{}:
      cfn(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, xa, c, cc, hsp, nok(c, hc))
    case Con{M.Entry{+k, +v}, +t}:
      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)))

# ---- backward: the entries before the cursor, reversed, then the rest ----


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):
  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))))

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)))):
  match r:
    case Tuple{h2, h3}:
      +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)
      +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)
      +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)
      %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), _))
      %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), _)))
      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, {==}, {==})

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)))):
  match p:
    case Tuple{+c2, Tuple{+ov, Tuple{+h1, r}}}:
      cbn2(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, bs, c, cc, hsp, c2, ov, h1, r)

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)))):
  match r:
    case Tuple{h2, h3}:
      +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, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}, bs), 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>, 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{}), hb))
      +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)
      +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)
      +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)
      +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)
      +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)))
      +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)))
      +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)))
      %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), _))
      %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), _)))
      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, {==})

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)))):
  match p:
    case Tuple{+c2, Tuple{+ov, Tuple{+h1, r}}}:
      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)

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{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, ~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, M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2))))):
  match r:
    case Tuple{g2, g3}:
      +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))
      +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)
      +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)
      +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)))
      +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))
      %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, _)))
      +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{}}))
      +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))))
      +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)))
      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))

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, 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, ~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, M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c2))))):
  match q:
    case Tuple{+c3, Tuple{+o3, Tuple{+g1, r}}}:
      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)

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, ~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, ~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)))):
  match r:
    case Tuple{h2, h3}:
      +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}), bs), SC.reverse(M.Entry<K, V>, t), k, v, bs, LL.snoc_append_cons(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}, bs), 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>, 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{}), hb))
      +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)
      +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)
      +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)
      %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), _))
      %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), _)))
      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)

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, ~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)))):
  match p:
    case Tuple{+c2, Tuple{+ov, Tuple{+h1, r}}}:
      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)

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(~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)))):
  match b:
    case True{}:
      cbt(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, bs, k, v, t, c, cc, hsp, hord, hbu, hb, p, kont)
    case False{}:
      cbs(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, bs, k, v, t, c, cc, hsp, hord, hbu, hb, p)


# the clear backward: every entry of the run before the cursor removed
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)))):
  match rr:
    case Nil{}:
      cbn(~K, ~V, ~cmp, ~o, ~nok, ~rok, l, lo2, hi2, x, bs, c, cc, hsp, nok(c, hc))
    case Con{M.Entry{+k, +v}, +t}:
      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)))