added lemma wfP_subset_mset[simp]

--- a/NEWS	Fri Oct 14 15:48:31 2022 +0100
+++ b/NEWS	Sat Oct 15 16:34:19 2022 +0200
@@ -46,6 +46,9 @@
       fimage_strict_mono
       wfP_pfsubset
 
+* Theory "HOL-Library.Multiset":
+  - Added lemma wfP_subset_mset[simp].
+
 
 New in Isabelle2022 (October 2022)
 ----------------------------------

--- 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"