PROOF.rot_lo.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 613-642 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=613&end_line=642

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

def rot_lo.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, +lo: O.OMap<K, V>, +hk: K,
  +hv: V, +hl: O.OMap<K, V>, +hh: O.OMap<K, V>, +khk: {cmp(k, hk) == LT{} : Cmp}
) -> {O.OMap.get(~K, ~V, ~cmp,
       O.OMap.bin(K, V, hk, hv, O.OMap.bin(K, V, k, v, lo, hl), hh), x)
      == O.OMap.get(~K, ~V, ~cmp, O.OBin{0, k, v, lo, O.OBin{0, hk, hv, hl, hh}}, x)
      : Maybe<&2, V>}:
  +inner = {O.OBin{0, k, v, lo, hl} : O.OMap<K, V>}
  +lhs = {O.OBin{0, hk, hv, inner, hh} : O.OMap<K, V>}
  split(c => {O.OMap.get(~K, ~V, ~cmp, lhs, x)
      == getc(~K, ~V, ~cmp, c, x, v, lo, O.OBin{0, hk, hv, hl, hh}) : Maybe<&2, V>},
    cmp(x, k),
    +e => Equal.trans(Maybe<&2, V>, O.OMap.get(~K, ~V, ~cmp, lhs, x),
      O.OMap.get(~K, ~V, ~cmp, inner, x), O.OMap.get(~K, ~V, ~cmp, lo, x),
      get.lt(~K, ~V, ~cmp, x, hk, hv, inner, hh, trans(x, k, hk, e, khk)),
      get.lt(~K, ~V, ~cmp, x, k, v, lo, hl, e)),
    e => rw(K, y => {O.OMap.get(~K, ~V, ~cmp, lhs, y) == Some{v} : Maybe<&2, V>},
      x, k, eq(x, k, e),
      Equal.trans(Maybe<&2, V>, O.OMap.get(~K, ~V, ~cmp, lhs, k),
        O.OMap.get(~K, ~V, ~cmp, inner, k), Some{v},
        get.lt(~K, ~V, ~cmp, k, hk, hv, inner, hh, khk),
        get.here(~K, ~V, ~cmp, ~refl, k, v, lo, hl))),
    e => split(c => {getc(~K, ~V, ~cmp, c, x, hv, inner, hh)
        == getc(~K, ~V, ~cmp, c, x, hv, hl, hh) : Maybe<&2, V>},
      cmp(x, hk),
      e2 => get.gt(~K, ~V, ~cmp, x, k, v, lo, hl, e),
      e2 => {==},
      e2 => {==}))

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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=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=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
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/omap.bend&name=OMap.get