--- a/Delete_prop.thy	Tue Jun 04 15:51:02 2013 +0800
+++ b/Delete_prop.thy	Thu Jun 06 08:00:20 2013 +0800
@@ -218,6 +218,11 @@
   current_msg_imp_current_msgq)
 done
 
+lemma not_deleted_imp_alive_cons:
+  "\<lbrakk>\<not> deleted obj (e # s); valid (e # s); alive s obj\<rbrakk> \<Longrightarrow> alive (e # s) obj"
+using not_deleted_imp_alive_app[where s = s and s' = "[e]" and obj = obj]
+by auto
+
 (*
 
 lemma nodel_imp_un_deleted: