def bool.and_r

bend-osdev-algo@0.1.0.0 · PROOF.bend:847

import bend-osdev-algo@0.1.0.0/PROOF.bend as PROOF

import Base

847def bool.and_r(a: Bool, -b: Bool, e: {Bool.and(a, b) == True{} : Bool}) -> {b == True{} : Bool}:
848  match a:
849    case True{}:
850      e
851    case False{}:
852      Empty.absurd({b == True{} : Bool}, absurd.ft(e))

Uses (4)

Used by (2)