PROOF.rot_hi.double.get2: def of bend-kit-collections@0.1.4.1
Import: import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF
Lines 775-815 of bend-kit-collections@0.1.4.1/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&start_line=775&end_line=815

import Base
import bend-kit-collections@0.1.4.1/omap.bend as O

def rot_hi.double.get2(
  ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~refl: Refl(~K, ~cmp), ~eq: Eq(~K, ~cmp),
  ~flip: Flip(~K, ~cmp), ~trans: Trans(~K, ~cmp),
  +x: K, +k: K, +v: V, +lk: K, +lv: V, +ll: O.OMap<K, V>, +mk: K, +mv: V,
  +ml: O.OMap<K, V>, +mh: O.OMap<K, V>, +hi: O.OMap<K, V>,
  +lkm: {cmp(lk, mk) == LT{} : Cmp}, +mkk: {cmp(mk, k) == LT{} : Cmp}
) -> {g(~K, ~V, ~cmp, O.OMap.bin(K, V, mk, mv, O.OMap.bin(K, V, lk, lv, ll, ml),
        O.OMap.bin(K, V, k, v, mh, hi)), x)
      == g(~K, ~V, ~cmp, O.OBin{0, k, v, O.OBin{0, lk, lv, ll, O.OBin{0, mk, mv, ml, mh}}, hi}, x)
      : Maybe<&2, V>}:
  +a = {O.OBin{0, lk, lv, ll, ml} : O.OMap<K, V>}
  +b = {O.OBin{0, k, v, mh, hi} : O.OMap<K, V>}
  +l = {O.OBin{0, mk, mv, a, b} : O.OMap<K, V>}
  +m = {O.OBin{0, mk, mv, ml, mh} : O.OMap<K, V>}
  +ln = {O.OBin{0, lk, lv, ll, m} : O.OMap<K, V>}
  split(c => {g(~K, ~V, ~cmp, l, x) == getc(~K, ~V, ~cmp, c, x, v, ln, hi) : Maybe<&2, V>},
    cmp(x, k),
    +e => split(c => {g(~K, ~V, ~cmp, l, x) == getc(~K, ~V, ~cmp, c, x, lv, ll, m) : Maybe<&2, V>},
      cmp(x, lk),
      +e2 => mtr(V, g(~K, ~V, ~cmp, l, x), g(~K, ~V, ~cmp, a, x), g(~K, ~V, ~cmp, ll, x),
        get.lt(~K, ~V, ~cmp, x, mk, mv, a, b, trans(x, lk, mk, e2, lkm)),
        get.lt(~K, ~V, ~cmp, x, lk, lv, ll, ml, e2)),
      e2 => rw(K, y => {g(~K, ~V, ~cmp, l, y) == Some{lv} : Maybe<&2, V>}, x, lk, eq(x, lk, e2),
        mtr(V, g(~K, ~V, ~cmp, l, lk), g(~K, ~V, ~cmp, a, lk), Some{lv},
          get.lt(~K, ~V, ~cmp, lk, mk, mv, a, b, lkm),
          get.here(~K, ~V, ~cmp, ~refl, lk, lv, ll, ml))),
      +e2 => split(c => {getc(~K, ~V, ~cmp, c, x, mv, a, b)
          == getc(~K, ~V, ~cmp, c, x, mv, ml, mh) : Maybe<&2, V>},
        cmp(x, mk),
        e3 => get.gt(~K, ~V, ~cmp, x, lk, lv, ll, ml, e2),
        e3 => {==},
        e3 => get.lt(~K, ~V, ~cmp, x, k, v, mh, hi, e))),
    e => rw(K, y => {g(~K, ~V, ~cmp, l, y) == Some{v} : Maybe<&2, V>}, x, k, eq(x, k, e),
      mtr(V, g(~K, ~V, ~cmp, l, k), g(~K, ~V, ~cmp, b, k), Some{v},
        get.gt(~K, ~V, ~cmp, k, mk, mv, a, b, gt_of_lt(~K, ~cmp, ~flip, mk, k, mkk)),
        get.here(~K, ~V, ~cmp, ~refl, k, v, mh, hi))),
    +e => mtr(V, g(~K, ~V, ~cmp, l, x), g(~K, ~V, ~cmp, b, x), g(~K, ~V, ~cmp, hi, x),
      get.gt(~K, ~V, ~cmp, x, mk, mv, a, b,
        gt_of_lt(~K, ~cmp, ~flip, mk, x,
          trans(mk, k, x, mkk, gt_flip(~K, ~cmp, ~flip, x, k, e)))),
      get.gt(~K, ~V, ~cmp, x, k, v, mh, hi, e)))

Uses (18):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=Eq
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=Flip
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=Refl
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=Trans
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=g
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=get.gt
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=get.here
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=get.lt
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=getc
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=gt_flip
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=gt_of_lt
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=mtr
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=rw
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=split
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/omap.bend&name=OMap
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/omap.bend&name=OMap.bin