def un.u32_cong

bend-osdev-u32@0.1.0.0 · PROOF.bend:829

import Base

829def un.u32_cong(-x: Word(32n), -y: Word(32n), e: {x == y : Word(32n)}) -> {U32{x} == U32{y} : U32}:
830  %e : {U32{x} == U32{_} : U32}
831  {==}