def nl

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

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

168# neither infinite nor NaN: the exponent field is not 2047
169def nl(+a: Bool, +d: Bool, +hi: {Bool.and(a, d) == False{} : Bool}, +hn: {Bool.and(a, Bool.not(d)) == False{} : Bool}) -> {a == False{} : Bool}:
170  match a d:
171    case True{} True{}:
172      NC.absurd_tf({True{} == False{} : Bool}, Equal.sym(Bool, True{}, False{}, hi))
173    case True{} False{}:
174      NC.absurd_tf({True{} == False{} : Bool}, Equal.sym(Bool, True{}, False{}, hn))
175    case False{} _:
176      {==}