def and_true_r

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/listops.bend:45

import Base

45def and_true_r(b: Bool) -> {Bool.and(b, True{}) == b : Bool}:
46  match b:
47    case True{}:
48      {==}
49    case False{}:
50      {==}