StorageAddressBounds.equal_values: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/storage_address_bounds.bend as StorageAddressBounds
Lines 74-77 of stelliferous@0.0.2.0/proofs/storage_address_bounds.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/storage_address_bounds.bend&start_line=74&end_line=77

import Base
import stelliferous@0.0.2.0/proofs/bounded_u32_arithmetic.bend as Arithmetic

def equal_values(+left: U32,+right: U32,equation: {U32.to_nat(left) == U32.to_nat(right) : Nat}) -> {left == right : U32}:
  %Arithmetic.native_roundtrip(left) : {_ == right : U32}
  %Arithmetic.native_roundtrip(right) : {U32.from_nat(U32.to_nat(left)) == _ : U32}
  Equal.cong(Nat,U32,U32.from_nat,U32.to_nat(left),U32.to_nat(right),equation)

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/bounded_u32_arithmetic.bend&name=native_roundtrip