~/jendhub

def bo.and_r

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:1711

import bend-osdev-cipher-modes@0.1.0.0/PROOF.bend as PROOF
import Base

1711def bo.and_r(+a: Bool, +b: Bool) -> {Bool.and(a, b) == True{} : Bool} -> {b == True{} : Bool}:
1712  match a:
1713    case False{}:
1714      h => bo.absurd({b == True{} : Bool}, h)
1715    case True{}:
1716      h => h

Uses (3)

Used by (1)