def un.bool_eq

bend-osdev-u32@0.1.0.0 · PROOF.bend:435

import Base

435def un.bool_eq(x: Bool, y: Bool, e: {Bool.cmp(x, y) == EQ{} : Cmp}) -> {x == y : Bool}:
436  match x y:
437    case False{} False{}:
438      {==}
439    case False{} True{}:
440      Empty.absurd({False{} == True{} : Bool}, un.lt_eq(e))
441    case True{} False{}:
442      Empty.absurd({True{} == False{} : Bool}, un.gt_eq(e))
443    case True{} True{}:
444      {==}