def nat_unique

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

import Base

124def nat_unique(+a: Nat, +b: Nat,
125    +first: {a == b : Nat}, +second: {a == b : Nat}) ->
126    {first == second : {a == b : Nat}}:
127    +first_code = nat_encode(a, b, first)
128    +second_code = nat_encode(a, b, second)
129    codes_same = nat_code_unique(a, b, first_code, second_code)
130    decoded_same = Equal.cong(nat_code(a, b), {a == b : Nat},
131        code => nat_decode(a, b, code), first_code, second_code, codes_same)
132    Equal.trans({a == b : Nat}, first, nat_decode(a, b, first_code), second,
133        Equal.sym({a == b : Nat}, nat_decode(a, b, first_code), first,
134            nat_decode_encode(a, b, first)),
135        Equal.trans({a == b : Nat}, nat_decode(a, b, first_code),
136            nat_decode(a, b, second_code), second, decoded_same,
137            nat_decode_encode(a, b, second)))