PROOF.w_pos: def of bend-kit-collections@0.1.4.1
Import: import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF
Lines 1220-1225 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=1220&end_line=1225

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

def w_pos(-K: Data, -V: Data, t: O.OMap<K, V>) -> Ord.LE(1n, W(K, V, t)):
  match t:
    case O.OTip{}:
      {==}
    case O.OBin{s, k, v, +lo, +hi}:
      pos_add(W(K, V, lo), W(K, V, hi), w_pos(K, V, lo))

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=W
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=pos_add
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=LE
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/omap.bend&name=OMap