def bool_code_unique

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

import Base

39def bool_code_unique(+a: Bool, +b: Bool,
40    +first: bool_code(a, b), second: bool_code(a, b)) ->
41    {first == second : bool_code(a, b)}:
42    match a b:
43        case False{} False{}:
44            match first second:
45                case Unit{} Unit{}: {==}
46        case True{} True{}:
47            match first second:
48                case Unit{} Unit{}: {==}
49        case False{} True{}:
50            Empty.absurd({first == second : bool_code(a, b)}, first)
51        case True{} False{}:
52            Empty.absurd({first == second : bool_code(a, b)}, first)