def wu.ve

bend-osdev-word64@0.1.1.0 · PROOF_text.bend:19

import Base

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