def aes_bytes_cert_is_some

qasim-bend-kit@0.1.0.2 · PROOF.bend:481

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES

481def aes_bytes_cert_is_some(+bytes: List<&2, U32>,
482    evidence: {AES.bytes_valid(bytes) == True{} : Bool}) ->
483    {Maybe.is_some(&0, {AES.bytes_valid(bytes) == True{} : Bool},
484        AES.aes_bytes_valid_proof(bytes)) == True{} : Bool}:
485    Equal.trans(Bool,
486        Maybe.is_some(&0, {AES.bytes_valid(bytes) == True{} : Bool},
487            AES.aes_bytes_valid_proof(bytes)),
488        AES.bytes_valid(bytes), True{},
489        aes_bytes_valid_status(bytes, AES.bytes_valid(bytes), {==}),
490        evidence)