[STATEMENT]
lemma unat_ucast_10_32 :
  fixes x :: "10 word"
  shows "unat (ucast x :: word32) = unat x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat (UCAST(10 \<rightarrow> 32) x) = unat x
[PROOF STEP]
by transfer simp