def h.nk

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

import Base

2079# eq(k, key) is False when key is equal to k2 and eq(k, k2) is False.
2080def h.nk(
2081  ~K: Data, ~eq: K -> K -> Bool,
2082  ~sound: @x: K -> @y: K -> {eq(x, y) == True{} : Bool} -> {x == y : K},
2083  +k2: K, +key: K, +k: K, e: {eq(k2, key) == True{} : Bool}, ne: {eq(k, k2) == False{} : Bool}
2084) -> {eq(k, key) == False{} : Bool}:
2085  rw(K, z => {eq(k, z) == False{} : Bool}, key, k2, Equal.sym(K, k2, key, sound(k2, key, e)), ne)