def not_t

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:691

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW

691def not_t(+b: Bool, +h: {Bool.not(b) == True{} : Bool}) -> {b == False{} : Bool}:
692  match b:
693    case True{}:
694      Empty.absurd({True{} == False{} : Bool}, LW.true_ne_false(Equal.sym(Bool, False{}, True{}, h)))
695    case False{}:
696      {==}