def false_of

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/aead.bend:437

import Base

437def false_of(+b: Bool, f: {b == True{} : Bool} -> Empty) -> {b == False{} : Bool}:
438  match b:
439    case True{}:
440      Empty.absurd({True{} == False{} : Bool}, f({==}))
441    case False{}:
442      {==}