def u32_natural_injective

bendtorch-core@0.1.0.0 · src/tensor/word_injective.bend:89

import Base

89def u32_natural_injective(+left: U32, +right: U32) ->
90  {U32.to_nat(left) == U32.to_nat(right) : Nat} -> {left == right : U32}:
91  match left right:
92    case U32{+lw} U32{+rw}:
93      equal => Equal.cong(Word(32n), U32, w => U32{w}, lw, rw, word_natural_injective(32n, lw, rw)(equal))