[STATEMENT]
lemma Rep_uint16'_code [code]: "Rep_uint16' x = (BITS n. bit x n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_uint16' x = (BITS n. bit x n)
[PROOF STEP]
by transfer (simp add: set_bits_bit_eq)