def h.bool_r

bend-kit-collections@0.1.4.1 · PROOF.bend:2646

import Base
import bend-kit-collections@0.1.4.1/hmap.bend as M

2646def h.bool_r(-A: Type, b: Bool, -x: A, -y1: A, -y2: A, e: {y1 == y2 : A})
2647  -> {M.HMap.bool(A, b, u => x, u => y1) == M.HMap.bool(A, b, u => x, u => y2) : A}:
2648  match b:
2649    case True{}:
2650      {==}
2651    case False{}:
2652      e