def ucmp_eq

bend-kit-collections@0.1.4.1 · PROOF.bend:3997

import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF

import Base
import bend-kit-lemmas@0.1.1.0/lemmas.bend as Lemmas

3997def ucmp_eq(+x: U32, +y: U32, e: {U32.cmp(x, y) == EQ{} : Cmp}) -> {x == y : U32}:
3998  Lemmas.u32_to_nat_inj(x, y, ncmp_eq(U32.to_nat(x), U32.to_nat(y),
3999    Equal.trans(Cmp, Nat.cmp(U32.to_nat(x), U32.to_nat(y)), U32.cmp(x, y), EQ{}, ucmp_nat(x, y), e)))

Uses (9)

Used by (2)