def cert_unique

qasim-bend-kit@0.1.0.2 · proof/JSON_PrimitiveProof.bend:40

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

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