def h.ne_f.c

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

import Base

2060# eq(k, k2) is False when k2 != k.
2061def h.ne_f.c(
2062  ~K: Data, ~eq: K -> K -> Bool,
2063  ~sound: @x: K -> @y: K -> {eq(x, y) == True{} : Bool} -> {x == y : K},
2064  +k2: K, +k: K, ne: {k2 != k : K}, b: Bool, eb: {b == eq(k, k2) : Bool}
2065) -> {b == False{} : Bool}:
2066  match b:
2067    case True{}:
2068      Empty.absurd({True{} == False{} : Bool}, ne(Equal.sym(K, k, k2, sound(k, k2, h.sb(True{}, eq(k, k2), eb)))))
2069    case False{}:
2070      {==}