def notinj

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

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW

130def notinj(+a: Bool, +b: Bool, +h: {Bool.not(a) == Bool.not(b) : Bool}) -> {a == b : Bool}:
131  match a b:
132    case True{} True{}:
133      {==}
134    case True{} False{}:
135      Empty.absurd({True{} == False{} : Bool}, LW.true_ne_false(Equal.sym(Bool, False{}, True{}, h)))
136    case False{} True{}:
137      Empty.absurd({False{} == True{} : Bool}, LW.true_ne_false(h))
138    case False{} False{}:
139      {==}