src/HOL/Option.thy

--- a/src/HOL/Option.thy	Fri Apr 20 07:36:58 2018 +0000
+++ b/src/HOL/Option.thy	Fri Apr 20 07:36:59 2018 +0000
@@ -311,6 +311,9 @@
 
 end
 
+lemma finite_range_Some: "finite (range (Some :: 'a \<Rightarrow> 'a option)) = finite (UNIV :: 'a set)"
+  by (auto dest: finite_imageD intro: inj_Some)
+
 
 subsection \<open>Transfer rules for the Transfer package\<close>