def not_f

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64laws.bend:95

import Base

95def not_f(+x: Bool, +h: {Bool.not(x) == False{} : Bool}) -> {x == True{} : Bool}:
96  match x:
97    case True{}:
98      {==}
99    case False{}:
100      Empty.absurd({False{} == True{} : Bool}, true_ne_false(h))