def or_ff

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64next.bend:55

import Base

55def or_ff(+a: Bool, +b: Bool, +ha: {a == False{} : Bool}, +hb: {b == False{} : Bool}) -> {Bool.or(a, b) == False{} : Bool}:
56  Equal.trans(Bool, Bool.or(a, b), Bool.or(False{}, b), False{}, Equal.cong(Bool, Bool, t => Bool.or(t, b), a, False{}, ha), hb)