def AP.and_r

bend-osdev-array@0.1.0.1 · PROOF.bend:528

import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF

import Base

528def AP.and_r(a: Bool, -b: Bool, e: {Bool.and(a, b) == True{} : Bool}) -> {b == True{} : Bool}:
529  match a:
530    case True{}:
531      e
532    case False{}:
533      Empty.absurd({b == True{} : Bool}, AP.ft(e))

Uses (4)

Used by (4)