def h.size_leaf

bend-kit-collections@0.1.4.1 · PROOF.bend:2802

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

2802def h.size_leaf(-K: Data, -V: Data, +o: U32, xs: List<&2, M.Entry<K, V>>)
2803  -> {h.len(K, V, xs) == h.Sz(K, V, M.HMap.leaf(K, V, o, xs)) : Nat}:
2804  match xs:
2805    case Nil{}:
2806      {==}
2807    case Con{e, rest}:
2808      {==}