PROOF.rot_hi.single.get: def of bend-kit-collections@0.1.4.1
Import: import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF
Lines 747-773 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=747&end_line=773

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

def rot_hi.single.get(
  ~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>, +lh: O.OMap<K, V>,
  +hi: O.OMap<K, V>, +lkk: {cmp(lk, k) == LT{} : Cmp}
) -> {g(~K, ~V, ~cmp, O.OMap.bin(K, V, lk, lv, ll, O.OMap.bin(K, V, k, v, lh, hi)), x)
      == g(~K, ~V, ~cmp, O.OBin{0, k, v, O.OBin{0, lk, lv, ll, lh}, hi}, x) : Maybe<&2, V>}:
  +b = {O.OBin{0, k, v, lh, hi} : O.OMap<K, V>}
  +l = {O.OBin{0, lk, lv, ll, b} : O.OMap<K, V>}
  +ln = {O.OBin{0, lk, lv, ll, lh} : 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 => {getc(~K, ~V, ~cmp, c, x, lv, ll, b)
        == getc(~K, ~V, ~cmp, c, x, lv, ll, lh) : Maybe<&2, V>},
      cmp(x, lk),
      e2 => {==},
      e2 => {==},
      e2 => get.lt(~K, ~V, ~cmp, x, k, v, lh, 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, lk, lv, ll, b, gt_of_lt(~K, ~cmp, ~flip, lk, k, lkk)),
        get.here(~K, ~V, ~cmp, ~refl, k, v, lh, 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, lk, lv, ll, b,
        gt_of_lt(~K, ~cmp, ~flip, lk, x,
          trans(lk, k, x, lkk, gt_flip(~K, ~cmp, ~flip, x, k, e)))),
      get.gt(~K, ~V, ~cmp, x, k, v, lh, 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