diff -r a627d67434db -r cee0b9fccf6f src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Wed Oct 12 14:50:24 2022 +0200
+++ b/src/HOL/Library/FSet.thy	Thu Oct 13 10:44:27 2022 +0200
@@ -556,6 +556,31 @@
 lemma subset_fimage_iff: "(B |\<subseteq>| f|`|A) = (\<exists> AA. AA |\<subseteq>| A \<and> B = f|`|AA)"
 by transfer (metis mem_Collect_eq rev_finite_subset subset_image_iff)
 
+lemma fimage_strict_mono:
+  assumes "inj_on f (fset B)" and "A |\<subset>| B"
+  shows "f |`| A |\<subset>| f |`| B"
+  \<comment> \<open>TODO: Configure transfer framework to lift @{thm Fun.inj_on_strict_subset}.\<close>
+proof (rule pfsubsetI)
+  from \<open>A |\<subset>| B\<close> have "A |\<subseteq>| B"
+    by (rule pfsubset_imp_fsubset)
+  thus "f |`| A |\<subseteq>| f |`| B"
+    by (rule fimage_mono)
+next
+  from \<open>A |\<subset>| B\<close> have "A |\<subseteq>| B" and "A \<noteq> B"
+    by (simp_all add: pfsubset_eq)
+
+  have "fset A \<noteq> fset B"
+    using \<open>A \<noteq> B\<close>
+    by (simp add: fset_cong)
+  hence "f ` fset A \<noteq> f ` fset B"
+    using \<open>A |\<subseteq>| B\<close>
+    by (simp add: inj_on_image_eq_iff[OF \<open>inj_on f (fset B)\<close>] less_eq_fset.rep_eq)
+  hence "fset (f |`| A) \<noteq> fset (f |`| B)"
+    by (simp add: fimage.rep_eq)
+  thus "f |`| A \<noteq> f |`| B"
+    by (simp add: fset_cong)
+qed
+
 
 subsubsection \<open>bounded quantification\<close>