# HG changeset patch
# User nipkow
# Date 1699476284 -3600
# Node ID 9e43ab263d338f586dbf968e11a1b9cf6f7162de
# Parent  7847cbfe3a62db22b6a5f383eafcc66c050961e5
added lemma

diff -r 7847cbfe3a62 -r 9e43ab263d33 src/HOL/Library/NList.thy
--- 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)