F64next.notinj: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64next.bend as F64next
Lines 130-139 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64next.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64next.bend&start_line=130&end_line=139

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

def notinj(+a: Bool, +b: Bool, +h: {Bool.not(a) == Bool.not(b) : Bool}) -> {a == b : Bool}:
  match a b:
    case True{} True{}:
      {==}
    case True{} False{}:
      Empty.absurd({True{} == False{} : Bool}, LW.true_ne_false(Equal.sym(Bool, False{}, True{}, h)))
    case False{} True{}:
      Empty.absurd({False{} == True{} : Bool}, LW.true_ne_false(h))
    case False{} False{}:
      {==}

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend&name=true_ne_false