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