def nat_code_unique

qasim-bend-kit@0.1.0.2 · proof/AES_CertificateProof.bend:111

import Base

111def nat_code_unique(+a: Nat, +b: Nat,
112    +first: nat_code(a, b), second: nat_code(a, b)) ->
113    {first == second : nat_code(a, b)}:
114    match a b:
115        case 0n 0n:
116            match first second:
117                case Unit{} Unit{}: {==}
118        case 0n 1n+q:
119            Empty.absurd({first == second : nat_code(a, b)}, first)
120        case 1n+p 0n:
121            Empty.absurd({first == second : nat_code(a, b)}, first)
122        case 1n+p 1n+q: nat_code_unique(p, q, first, second)