def wu.ve

bend-osdev-word64@0.1.1.0 · PROOF_mul.bend:17

import Base

17def wu.ve(+w: Word(32n)) -> {Word.to_nat(32n, w) == U32.to_nat(U32{w}) : Nat}:
18  {==}