def aes_maybe_cert_reconstruct

qasim-bend-kit@0.1.0.2 · proof/AES_EnvelopeProof.bend:765

import Base

765def aes_maybe_cert_reconstruct(A: Type, cert: Maybe<&0, A>,
766    present: {Maybe.is_some(&0, A, cert) == True{} : Bool}) ->
767    {cert == Some{aes_maybe_cert_value(A, cert, present)} : Maybe<&0, A>}:
768    match cert:
769        case None{}:
770            Empty.absurd({None{} ==
771                Some{aes_maybe_cert_value(A, None{}, present)} :
772                Maybe<&0, A>}, aes_false_true(present))
773        case Some{value}: {==}