def and_l

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64cmp.bend:140

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC

140def and_l(+a: Bool, +b: Bool, +h: {Bool.and(a, b) == True{} : Bool}) -> {a == True{} : Bool}:
141  match a:
142    case True{}:
143      {==}
144    case False{}:
145      NC.absurd_tf({False{} == True{} : Bool}, h)