def gt.u32_cong

bend-osdev-gf@0.1.1.0 · proof_tab.bend:43

import Base

43def gt.u32_cong(-x: Word(32n), -y: Word(32n), e: {x == y : Word(32n)}) -> {U32{x} == U32{y} : U32}:
44  %e : {U32{x} == U32{_} : U32}
45  {==}