def eq_nat

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32laws.bend:99

import Base

99def eq_nat(+x: U32, +y: U32) -> {U32.is_eq(x, y) == Nat.is_eq(v(x), v(y)) : Bool}:
100  eq_c(x, y, U32.is_eq(x, y), {==}, Nat.is_eq(v(x), v(y)), {==})