def h.bsel

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

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

2654def h.bsel(
2655  -A: Type, b: Bool, -x: A, -y: A, -z: A,
2656  ht: {b == True{} : Bool} -> {x == z : A}, hf: {b == False{} : Bool} -> {y == z : A}
2657) -> {M.HMap.bool(A, b, u => x, u => y) == z : A}:
2658  match b:
2659    case True{}:
2660      ht({==})
2661    case False{}:
2662      hf({==})