def un.vc

bend-osdev-u32@0.1.0.0 · PROOF.bend:338

import Base

338def un.vc(-p: Nat, b: Bool, -t: Word(p)) -> {un.bv(b, Word.to_nat(p, t)) == Word.to_nat(1n+p, WCon{b, t}) : Nat}:
339  match b:
340    case False{}:
341      {==}
342    case True{}:
343      {==}