PROOFText.wv.ve: def of bend-osdev-word64@0.1.1.0
Import: import bend-osdev-word64@0.1.1.0/PROOF_text.bend as PROOFText
Lines 33-34 of bend-osdev-word64@0.1.1.0/PROOF_text.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&start_line=33&end_line=34

import Base
import bend-osdev-word64@0.1.1.0/word64.bend as W
import bend-osdev-word64@0.1.1.0/proof_value.bend as P

def wv.ve(+h: Word(32n), +l: Word(32n)) -> {P.wv.V(32n, h, l) == W.W64.to_nat(W.W64{U32{h}, U32{l}}) : Nat}:
  {==}

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_value.bend&name=wv.V
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.to_nat