AES256GCM.aes_bool_true_proof: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES256GCM
Lines 325-331 of qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&start_line=325&end_line=331

import Base

def aes_bool_true_proof(+x: U32, b: Bool,
                        link: {b == U32.is_lt(x, 256) : Bool}) -> Maybe<&0, {U32.is_lt(x, 256) == True{} : Bool}>:
    match b:
        case False{}: None{}
        case True{}:
            Some{Equal.trans(Bool, U32.is_lt(x, 256), b, True{},
                Equal.sym(Bool, b, U32.is_lt(x, 256), link), {==})}

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt