--- a/RTree.thy	Wed Jan 06 20:46:14 2016 +0800
+++ b/RTree.thy	Wed Jan 06 16:34:26 2016 +0000
@@ -154,6 +154,7 @@
 lemma index_minimize:
   assumes "P (i::nat)"
   obtains j where "P j" and "\<forall> k < j. \<not> P k" 
+using assms
 proof -
   have "\<exists> j. P j \<and> (\<forall> k < j. \<not> P k)"
   using assms