def bool_unique

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

import Base

54def bool_unique(+a: Bool, +b: Bool,
55    +first: {a == b : Bool}, +second: {a == b : Bool}) ->
56    {first == second : {a == b : Bool}}:
57    +first_code = bool_encode(a, b, first)
58    +second_code = bool_encode(a, b, second)
59    codes_same = bool_code_unique(a, b, first_code, second_code)
60    decoded_same = Equal.cong(bool_code(a, b), {a == b : Bool},
61        code => bool_decode(a, b, code), first_code, second_code, codes_same)
62    Equal.trans({a == b : Bool}, first, bool_decode(a, b, first_code), second,
63        Equal.sym({a == b : Bool}, bool_decode(a, b, first_code), first,
64            bool_decode_encode(a, b, first)),
65        Equal.trans({a == b : Bool}, bool_decode(a, b, first_code),
66            bool_decode(a, b, second_code), second, decoded_same,
67            bool_decode_encode(a, b, second)))