def AP.and_l

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

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

import Base

521def AP.and_l(a: Bool, -b: Bool, e: {Bool.and(a, b) == True{} : Bool}) -> {a == True{} : Bool}:
522  match a:
523    case True{}:
524      {==}
525    case False{}:
526      Empty.absurd({False{} == True{} : Bool}, AP.ft(e))

Uses (4)

Used by (5)