~/jendhub

def bool.and_l

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

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

840def bool.and_l(a: Bool, -b: Bool, e: {Bool.and(a, b) == True{} : Bool}) -> {a == True{} : Bool}:
841  match a:
842    case True{}:
843      {==}
844    case False{}:
845      Empty.absurd({False{} == True{} : Bool}, absurd.ft(e))

Uses (4)

Used by (1)