def h.elen_del_hit.c

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

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

2234def h.elen_del_hit.c(
2235  ~K: Data, ~V: Data, ~eq: K -> K -> Bool, +key: K, +val: V,
2236  +rest: List<&2, M.Entry<K, V>>, +k: K, -w: V, b: Bool,
2237  hit: {h.egc(~K, ~V, ~eq, b, val, rest, k) == Some{w} : Maybe<&2, V>},
2238  ih: {M.HMap.entries.get(~K, ~V, ~eq, rest, k) == Some{w} : Maybe<&2, V>}
2239    -> {1n+h.len(K, V, M.HMap.entries.del(~K, ~V, ~eq, rest, k)) == h.len(K, V, rest) : Nat}
2240) -> {1n+h.len(K, V, h.edc(~K, ~V, ~eq, b, key, val, rest, k)) == 1n+h.len(K, V, rest) : Nat}:
2241  match b:
2242    case True{}:
2243      {==}
2244    case False{}:
2245      Equal.cong(Nat, Nat, x => 1n+x, 1n+h.len(K, V, M.HMap.entries.del(~K, ~V, ~eq, rest, k)),
2246        h.len(K, V, rest), ih(hit))