[STATEMENT]
lemma [code]:
  "card_UNIV TYPE('a :: enum) = card (set (Enum.enum :: 'a list))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card_UNIV TYPE('a) = card (set enum)
[PROOF STEP]
by (simp only: card_UNIV_def enum_UNIV)