def bool.and2
import bend-osdev-caps@0.1.0.0/PROOF.bend as PROOFimport Base
101def bool.and2(+x: Bool, +y: Bool) -> {x == True{} : Bool} -> {y == True{} : Bool} -> {Bool.and(x, y) == True{} : Bool}:
102 match x:
103 case True{}:
104 hx => hy => hy
105 case False{}:
106 hx => hy => bits.absurd(Bool.and(False{}, y), hx)