def bool_and_true_right

qasim-bend-kit@0.1.0.2 · proof/AES_LengthLimitProof.bend:5

import Base
import qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend as ZipLengthProof

5def bool_and_true_right(+a: Bool, +b: Bool,
6    both: {Bool.and(a, b) == True{} : Bool}) -> {b == True{} : Bool}:
7    match a b:
8        case False{} False{}:
9            Empty.absurd({False{} == True{} : Bool},
10                ZipLengthProof.false_true(both))
11        case False{} True{}: {==}
12        case True{} False{}:
13            Empty.absurd({False{} == True{} : Bool},
14                ZipLengthProof.false_true(both))
15        case True{} True{}: {==}