AESCertificateProof.nat_unique: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_CertificateProof.bend as AESCertificateProof
Lines 124-137 of qasim-bend-kit@0.1.0.2/proof/AES_CertificateProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_CertificateProof.bend&start_line=124&end_line=137

import Base

def nat_unique(+a: Nat, +b: Nat,
    +first: {a == b : Nat}, +second: {a == b : Nat}) ->
    {first == second : {a == b : Nat}}:
    +first_code = nat_encode(a, b, first)
    +second_code = nat_encode(a, b, second)
    codes_same = nat_code_unique(a, b, first_code, second_code)
    decoded_same = Equal.cong(nat_code(a, b), {a == b : Nat},
        code => nat_decode(a, b, code), first_code, second_code, codes_same)
    Equal.trans({a == b : Nat}, first, nat_decode(a, b, first_code), second,
        Equal.sym({a == b : Nat}, nat_decode(a, b, first_code), first,
            nat_decode_encode(a, b, first)),
        Equal.trans({a == b : Nat}, nat_decode(a, b, first_code),
            nat_decode(a, b, second_code), second, decoded_same,
            nat_decode_encode(a, b, second)))

Uses (9):
  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.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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/AES_CertificateProof.bend&name=nat_code
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_CertificateProof.bend&name=nat_code_unique
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_CertificateProof.bend&name=nat_decode
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_CertificateProof.bend&name=nat_decode_encode
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_CertificateProof.bend&name=nat_encode