PROOF.h.size_join: def of bend-kit-collections@0.1.4.1
Import: import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF
Lines 2835-2849 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=2835&end_line=2849

import Base
import bend-kit-collections@0.1.4.1/hmap.bend as M

def h.size_join(-K: Data, -V: Data, lo: M.HMap<K, V>, hi: M.HMap<K, V>)
  -> {Nat.add(h.Sz(K, V, lo), h.Sz(K, V, hi)) == h.Sz(K, V, M.HMap.join(K, V, lo, hi)) : Nat}:
  match lo:
    case M.HNil{}:
      match hi:
        case M.HNil{}:
          {==}
        case M.HLeaf{a, b}:
          {==}
        case M.HBranch{a, b}:
          {==}
    case M.HLeaf{a, b}:
      {==}
    case M.HBranch{a, b}:
      {==}

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=h.Sz
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/hmap.bend&name=HMap
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/hmap.bend&name=HMap.join