--- a/src/HOL/Library/NList.thy Thu Oct 26 20:41:42 2023 +0200
+++ b/src/HOL/Library/NList.thy Fri Oct 27 08:16:16 2023 +0200
@@ -44,6 +44,9 @@
lemma Cons_in_nlists_Suc [iff]: "(x#xs \<in> nlists (Suc n) A) \<longleftrightarrow> (x\<in>A \<and> xs \<in> nlists n A)"
unfolding nlists_def by (auto)
+lemma nlists_Suc: "nlists (Suc n) A = (\<Union>a\<in>A. (#) a ` nlists n A)"
+by(auto simp: set_eq_iff image_iff in_nlists_Suc_iff)
+
lemma nlists_not_empty: "A\<noteq>{} \<Longrightarrow> \<exists>xs. xs \<in> nlists n A"
by (induct "n") (auto simp: in_nlists_Suc_iff)