# HG changeset patch
# User nipkow
# Date 1698387376 -7200
# Node ID 35b2282fbc7737056d66146538dd623218981087
# Parent  98e164c3059f6aef0f2a6f439204ad576b6effd4
added lemma

diff -r 98e164c3059f -r 35b2282fbc77 src/HOL/Library/NList.thy
--- 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)