def equal_words
stelliferous@0.0.2.0 · proofs/storage_address_bounds.bend:79
import stelliferous@0.0.2.0/proofs/storage_address_bounds.bend as StorageAddressBounds
import Base
import stelliferous@0.0.2.0/proofs/nat_order.bend as Order
import stelliferous@0.0.2.0/proofs/u32_comparison.bend as Comparison
79def equal_words(+left: U32,+right: U32,equation: {U32.is_eq(left,right) == True{} : Bool}) -> {left == right : U32}:
80 equal_values(left,right,Order.equal_of_is_eq(U32.to_nat(left),U32.to_nat(right),
81 %Comparison.eq(left,right) : {_ == True{} : Bool}
82 equation))