def bool_cmp_eq

lawful-words@0.1.0.0 · proof_word.bend:253

import Base

253def bool_cmp_eq(+a: Bool, +b: Bool, e: {Bool.cmp(a, b) == EQ{} : Cmp}) -> {a == b : Bool}:
254  match a b:
255    case False{} False{}:
256      {==}
257    case False{} True{}:
258      Empty.absurd({False{} == True{} : Bool}, lt_ne_eq(e))
259    case True{} False{}:
260      Empty.absurd({True{} == False{} : Bool}, gt_ne_eq(e))
261    case True{} True{}:
262      {==}