def h.wf_fresh

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

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

3699# put and del keep the map well formed.
3700def h.wf_fresh(~K: Data, ~V: Data, ~hash: K -> U32, ~eq: K -> K -> Bool, p: Nat, +k: K, +v: V)
3701  -> {h.WF(~K, ~V, ~hash, ~eq, p, M.HLeaf{hash(k), [M.Entry{k, v}]}) == True{} : Bool}:
3702  match p:
3703    case 0n:
3704      {==}
3705    case 1n+q:
3706      %h.sb(U32.is_eq(hash(k), hash(k)), True{}, h.u_refl(hash(k)))
3707        : {Bool.and(Bool.and(_, True{}), True{}) == True{} : Bool}
3708      {==}