--- a/src/HOL/Library/NList.thy	Wed Nov 08 16:05:22 2023 +0100
+++ b/src/HOL/Library/NList.thy	Wed Nov 08 21:44:44 2023 +0100
@@ -20,6 +20,9 @@
 lemma nlistsE_length [simp]: "xs \<in> nlists n A \<Longrightarrow> size xs = n"
   by (simp add: nlists_def)
 
+lemma in_nlists_UNIV: "xs \<in> nlists k UNIV \<longleftrightarrow> length xs = k"
+unfolding nlists_def by(auto)
+
 lemma less_lengthI: "\<lbrakk> xs \<in> nlists n A; p < n \<rbrakk> \<Longrightarrow> p < size xs"
 by (simp)