src/HOL/Library/NList.thy

--- a/src/HOL/Library/NList.thy	Thu Aug 11 05:50:48 2022 +0200
+++ b/src/HOL/Library/NList.thy	Thu Aug 11 10:11:21 2022 +0200
@@ -95,4 +95,7 @@
 lemma nlists_replicateI [intro]: "x \<in> A \<Longrightarrow> replicate n x \<in> nlists n A"
  by (induct n) auto
 
+lemma nlists_set[code]: "nlists n (set xs) = set (List.n_lists n xs)"
+unfolding nlists_def by (rule sym, induct n) (auto simp: image_iff length_Suc_conv)
+
 end