def and_left

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/logic.bend:19

import Base

19def and_left(a: Bool, b: Bool, e: {Bool.and(a, b) == True{} : Bool}) -> {a == True{} : Bool}:
20  match a:
21    case False{}:
22      Empty.absurd({False{} == True{} : Bool}, false_true(e))
23    case True{}:
24      {==}