PROOF.h.bool_l: def of bend-kit-collections@0.1.4.1
Import: import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF
Lines 2638-2644 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=2638&end_line=2644

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

def h.bool_l(-A: Type, b: Bool, -x1: A, -x2: A, -y: A, e: {x1 == x2 : A})
  -> {M.HMap.bool(A, b, u => x1, u => y) == M.HMap.bool(A, b, u => x2, u => y) : A}:
  match b:
    case True{}:
      e
    case False{}:
      {==}

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