def and_l

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64sqrt.bend:150

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32.bend as U32P

150def and_l(+a: Bool, +b: Bool, +h: {Bool.and(a, b) == True{} : Bool}) -> {a == True{} : Bool}:
151  match a:
152    case True{}:
153      {==}
154    case False{}:
155      Empty.absurd({False{} == True{} : Bool}, U32P.true_ne_false(Equal.sym(Bool, False{}, True{}, h)))