def internal_and_left

bend-mathlib@0.8.1.0 · list.bend:725

import Base
import bend-mathlib@0.8.1.0/nat.bend as MNat

725def internal_and_left(a: Bool, -b: Bool, h: {Bool.and(a, b) == True{} : Bool}) -> {a == True{} : Bool}:
726  match a:
727    case False{}:
728      Empty.absurd({False{} == True{} : Bool}, MNat.internal_false_ne_true(h))
729    case True{}:
730      {==}