~/jendhub

def bo.and_l

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

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

1718def bo.and_l(+a: Bool, +b: Bool) -> {Bool.and(a, b) == True{} : Bool} -> {a == True{} : Bool}:
1719  match a:
1720    case False{}:
1721      h => bo.absurd({False{} == True{} : Bool}, h)
1722    case True{}:
1723      h => {==}

Uses (3)

Used by (1)