AESEnvelopeProof.aes_nat_eq_is_some: 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 727-742 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=727&end_line=742

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

def aes_nat_eq_is_some(+a: Nat, +b: Nat,
    evidence: {a == b : Nat}) ->
    {Maybe.is_some(&0, {a == b : Nat},
        AES.aes_nat_eq_proof(a, b)) == True{} : Bool}:
    Equal.trans(Bool,
        Maybe.is_some(&0, {a == b : Nat}, AES.aes_nat_eq_proof(a, b)),
        Maybe.is_some(&0, {b == b : Nat}, AES.aes_nat_eq_proof(b, b)),
        True{},
        Equal.cong(Nat, Bool,
            value => Maybe.is_some(&0, {value == b : Nat},
                AES.aes_nat_eq_proof(value, b)),
            a, b, evidence),
        Equal.cong(Maybe<&0, {b == b : Nat}>, Bool,
            result => Maybe.is_some(&0, {b == b : Nat}, result),
            AES.aes_nat_eq_proof(b, b), Some{{==}},
            aes_nat_eq_self(b)))

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  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=Maybe.is_some
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=aes_nat_eq_proof
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend&name=aes_nat_eq_self