AESEnvelopeProof.aes_maybe_cert_reconstruct: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend as AESEnvelopeProof
Lines 765-773 of qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend&start_line=765&end_line=773

import Base

def aes_maybe_cert_reconstruct(A: Type, cert: Maybe<&0, A>,
    present: {Maybe.is_some(&0, A, cert) == True{} : Bool}) ->
    {cert == Some{aes_maybe_cert_value(A, cert, present)} : Maybe<&0, A>}:
    match cert:
        case None{}:
            Empty.absurd({None{} ==
                Some{aes_maybe_cert_value(A, None{}, present)} :
                Maybe<&0, A>}, aes_false_true(present))
        case Some{value}: {==}

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=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe.is_some
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend&name=aes_false_true
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend&name=aes_maybe_cert_value