def or_l

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64cmp.bend:154

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC

154def or_l(+a: Bool, +b: Bool, +h: {Bool.or(a, b) == False{} : Bool}) -> {a == False{} : Bool}:
155  match a:
156    case True{}:
157      NC.absurd_tf({True{} == False{} : Bool}, Equal.sym(Bool, True{}, False{}, h))
158    case False{}:
159      {==}