src/ZF/Constructible/Formula.thy
changeset 13328 703de709a64b
parent 13316 d16629fd0f95
child 13339 0f89104dd377
--- a/src/ZF/Constructible/Formula.thy	Tue Jul 09 23:03:21 2002 +0200
+++ b/src/ZF/Constructible/Formula.thy	Tue Jul 09 23:05:26 2002 +0200
@@ -523,11 +523,6 @@
 
 subsubsection{*The subset relation*}
 
-lemma lt_length_in_nat:
-   "[|x < length(xs); xs \<in> list(A)|] ==> x \<in> nat"
-apply (frule lt_nat_in_nat, typecheck) 
-done
-
 constdefs subset_fm :: "[i,i]=>i"
     "subset_fm(x,y) == Forall(Implies(Member(0,succ(x)), Member(0,succ(y))))"