def bool.and_l

bend-osdev-caps@0.1.0.0 · PROOF.bend:54

import bend-osdev-caps@0.1.0.0/PROOF.bend as PROOF
import Base

54def bool.and_l(+x: Bool, +y: Bool) -> {Bool.and(x, y) == True{} : Bool} -> {x == True{} : Bool}:
55  match x:
56    case True{}:
57      h => {==}
58    case False{}:
59      h => bits.absurd(False{}, h)

Uses (3)

Used by (4)