def h.bool_l

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

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

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