def and_r

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

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

147def and_r(+a: Bool, +b: Bool, +h: {Bool.and(a, b) == True{} : Bool}) -> {b == True{} : Bool}:
148  match a:
149    case True{}:
150      h
151    case False{}:
152      NC.absurd_tf({b == True{} : Bool}, h)