--- a/src/ZF/Induct/ListN.thy Tue Sep 27 16:51:35 2022 +0100
+++ b/src/ZF/Induct/ListN.thy Tue Sep 27 17:03:23 2022 +0100
@@ -24,7 +24,7 @@
lemma list_into_listn: "l \<in> list(A) \<Longrightarrow> <length(l),l> \<in> listn(A)"
by (induct set: list) (simp_all add: listn.intros)
-lemma listn_iff: "<n,l> \<in> listn(A) \<longleftrightarrow> l \<in> list(A) & length(l)=n"
+lemma listn_iff: "<n,l> \<in> listn(A) \<longleftrightarrow> l \<in> list(A) \<and> length(l)=n"
apply (rule iffI)
apply (erule listn.induct)
apply auto