def bool_and_true_left

qasim-bend-kit@0.1.0.2 · proof/AES_MaskedXorProof.bend:156

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

156def bool_and_true_left(+a: Bool, +b: Bool,
157    both: {Bool.and(a, b) == True{} : Bool}) -> {a == True{} : Bool}:
158    match a b:
159        case False{} False{}:
160            Empty.absurd({False{} == True{} : Bool},
161                ZipLengthProof.false_true(both))
162        case False{} True{}:
163            Empty.absurd({False{} == True{} : Bool},
164                ZipLengthProof.false_true(both))
165        case True{} False{}: {==}
166        case True{} True{}: {==}