def bool.and_l
import bend-osdev-caps@0.1.0.0/PROOF.bend as PROOFimport 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)