AESCertificateProof.bool_code_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 39-52 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=39&end_line=52

import Base

def bool_code_unique(+a: Bool, +b: Bool,
    +first: bool_code(a, b), second: bool_code(a, b)) ->
    {first == second : bool_code(a, b)}:
    match a b:
        case False{} False{}:
            match first second:
                case Unit{} Unit{}: {==}
        case True{} True{}:
            match first second:
                case Unit{} Unit{}: {==}
        case False{} True{}:
            Empty.absurd({first == second : bool_code(a, b)}, first)
        case True{} False{}:
            Empty.absurd({first == second : bool_code(a, b)}, first)

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_CertificateProof.bend&name=bool_code