JSONPrimitiveProof.cert_unique: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/JSON_PrimitiveProof.bend as JSONPrimitiveProof
Lines 40-45 of qasim-bend-kit@0.1.0.2/proof/JSON_PrimitiveProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_PrimitiveProof.bend&start_line=40&end_line=45

import Base
import qasim-bend-kit@0.1.0.2/libs/JSON.bend as J

def cert_unique(+text: String,
                +a: J.NumberCert<text>,
                +b: J.NumberCert<text>) -> {a == b : J.NumberCert<text>}:
    match a b:
        case J.Certified{x} J.Certified{y}:
            Equal.cong(J.NumberProof(text), J.NumberCert<text>, w => J.Certified{w}, x, y, proof_unique(J.number_valid(text), x, y))

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=NumberCert
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=NumberProof
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=number_valid
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_PrimitiveProof.bend&name=proof_unique