Require Import Coq.ZArith.ZArith.
Require Import Coq.micromega.Lia.
Require Import Coq.Bool.Bool.

Require Import bbv.Word.
Import Notations.

#[local] Open Scope nat_scope.
#[local] Open Scope word_scope.

Definition wucast {sz: nat} (sz': nat) (w: word sz) : word sz' :=
  ZToWord _ (uwordToZ w).