def round_trip
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32.bend as U32import Base
77def round_trip(+a: U32) -> {U32.from_nat(U32.to_nat(a)) == a : U32}:
78 round_trip_k(1n, {==}, 32n, {==}, a)
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32.bend as U32import Base
77def round_trip(+a: U32) -> {U32.from_nat(U32.to_nat(a)) == a : U32}:
78 round_trip_k(1n, {==}, 32n, {==}, a)