PROOF.h.bool_r: def of bend-kit-collections@0.1.4.1
Import: import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF
Lines 2646-2652 of bend-kit-collections@0.1.4.1/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&start_line=2646&end_line=2652

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

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

Uses (2):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/hmap.bend&name=HMap.bool