def h.egc2

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

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

2049def h.egc2(
2050  ~K: Data, ~V: Data, ~eq: K -> K -> Bool, c: Bool, +val: V,
2051  +xs: List<&2, M.Entry<K, V>>, +ys: List<&2, M.Entry<K, V>>, +k: K,
2052  e: {M.HMap.entries.get(~K, ~V, ~eq, xs, k) == M.HMap.entries.get(~K, ~V, ~eq, ys, k) : Maybe<&2, V>}
2053) -> {h.egc(~K, ~V, ~eq, c, val, xs, k) == h.egc(~K, ~V, ~eq, c, val, ys, k) : Maybe<&2, V>}:
2054  match c:
2055    case True{}:
2056      {==}
2057    case False{}:
2058      e