PROOF.aes_nat_eq_is_some: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/PROOF.bend as PROOF
Lines 417-428 of qasim-bend-kit@0.1.0.2/PROOF.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/PROOF.bend&start_line=417&end_line=428

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),
        aes_nat_eq_refl_is_some(b))

Uses (7):
  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.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/PROOF.bend&name=aes_nat_eq_refl_is_some
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=aes_nat_eq_proof