def not_t

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64clz.bend:178

import Base

178def not_t(+x: Bool, +h: {Bool.not(x) == True{} : Bool}) -> {x == False{} : Bool}:
179  match x:
180    case True{}:
181      Empty.absurd({True{} == False{} : Bool}, true_ne_false(Equal.sym(Bool, False{}, True{}, h)))
182    case False{}:
183      {==}