[STATEMENT]
lemma toEnum_of_nat[simp]: "n < 2 ^ LENGTH('a) \<Longrightarrow> (toEnum n :: 'a :: len word) = of_nat n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < 2 ^ LENGTH('a) \<Longrightarrow> toEnum n = word_of_nat n
[PROOF STEP]
by (simp add: toEnum_def length_word_enum enum_word_def)