src/HOL/Library/Multiset.thy

--- a/src/HOL/Library/Multiset.thy	Fri Oct 14 15:48:31 2022 +0100
+++ b/src/HOL/Library/Multiset.thy	Sat Oct 15 16:34:19 2022 +0200
@@ -1575,6 +1575,9 @@
 apply (clarsimp simp: measure_def inv_image_def mset_subset_size)
 done
 
+lemma wfP_subset_mset[simp]: "wfP (\<subset>#)"
+  by (rule wf_subset_mset_rel[to_pred])
+
 lemma full_multiset_induct [case_names less]:
 assumes ih: "\<And>B. \<forall>(A::'a multiset). A \<subset># B \<longrightarrow> P A \<Longrightarrow> P B"
 shows "P B"