AESCertificateProof.bool_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 54-67 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=54&end_line=67

import Base

def bool_unique(+a: Bool, +b: Bool,
    +first: {a == b : Bool}, +second: {a == b : Bool}) ->
    {first == second : {a == b : Bool}}:
    +first_code = bool_encode(a, b, first)
    +second_code = bool_encode(a, b, second)
    codes_same = bool_code_unique(a, b, first_code, second_code)
    decoded_same = Equal.cong(bool_code(a, b), {a == b : Bool},
        code => bool_decode(a, b, code), first_code, second_code, codes_same)
    Equal.trans({a == b : Bool}, first, bool_decode(a, b, first_code), second,
        Equal.sym({a == b : Bool}, bool_decode(a, b, first_code), first,
            bool_decode_encode(a, b, first)),
        Equal.trans({a == b : Bool}, bool_decode(a, b, first_code),
            bool_decode(a, b, second_code), second, decoded_same,
            bool_decode_encode(a, b, second)))

Uses (9):
  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.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_CertificateProof.bend&name=bool_code
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_CertificateProof.bend&name=bool_code_unique
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_CertificateProof.bend&name=bool_decode
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_CertificateProof.bend&name=bool_decode_encode
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_CertificateProof.bend&name=bool_encode