def h.sz_del_miss.lf

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

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

3626def h.sz_del_miss.lf(
3627  ~K: Data, ~V: Data, ~eq: K -> K -> Bool, +o: U32,
3628  +es: List<&2, M.Entry<K, V>>, +hk: U32, +k: K,
3629  b: Bool, eb: {b == U32.is_eq(o, hk) : Bool},
3630  miss: {M.HMap.bool(Maybe<&2, V>, U32.is_eq(o, hk), u => h.EG(~K, ~V, ~eq, es, k), u => None{}) == None{} : Maybe<&2, V>}
3631) -> {h.Sz(K, V, h.dl(~K, ~V, ~eq, b, o, es, k)) == h.len(K, V, es) : Nat}:
3632  match b:
3633    case True{}:
3634      %h.size_leaf(K, V, o, M.HMap.entries.del(~K, ~V, ~eq, es, k)) : {_ == h.len(K, V, es) : Nat}
3635      Equal.cong(List<&2, M.Entry<K, V>>, Nat, xs => h.len(K, V, xs), M.HMap.entries.del(~K, ~V, ~eq, es, k), es,
3636        h.edel_miss(~K, ~V, ~eq, es, k,
3637          rw(Bool, z => {M.HMap.bool(Maybe<&2, V>, z, u => h.EG(~K, ~V, ~eq, es, k), u => None{}) == None{} : Maybe<&2, V>},
3638            True{}, U32.is_eq(o, hk), eb, miss)))
3639    case False{}:
3640      {==}