def or_r

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

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

161def or_r(+a: Bool, +b: Bool, +h: {Bool.or(a, b) == False{} : Bool}) -> {b == False{} : Bool}:
162  match a:
163    case True{}:
164      NC.absurd_tf({b == False{} : Bool}, Equal.sym(Bool, True{}, False{}, h))
165    case False{}:
166      h