def AP.u32_cong

bend-osdev-array@0.1.0.1 · PROOF.bend:322

import Base

322def AP.u32_cong(-x: Word(32n), -y: Word(32n), e: {x == y : Word(32n)}) -> {U32{x} == U32{y} : U32}:
323  %e : {U32{x} == U32{_} : U32}
324  {==}