
diff -r ce964f0df281 -r 19d8783a30de src/HOL/Nominal/Examples/Contexts.thy
--- a/src/HOL/Nominal/Examples/Contexts.thy	Fri May 16 21:56:13 2008 +0200
+++ b/src/HOL/Nominal/Examples/Contexts.thy	Fri May 16 22:35:25 2008 +0200
@@ -141,8 +141,13 @@
   then show  "App (Lam [x].t) t' \<longrightarrow>x t[x::=t']" by simp
 qed (metis ctx_red_in_ctx filling.simps)+ (* found by SledgeHammer *)
 
+lemma ctx_existence:
+  assumes a: "t \<longrightarrow>o t'"
+  shows "\<exists>C s s'. t = C\<lbrakk>s\<rbrakk> \<and> t' = C\<lbrakk>s'\<rbrakk> \<and> s \<longrightarrow>o s'"
+using a
+by (induct) (metis cong_red.intros filling.simps)+
 
-section {* We now use context in a CBV list machine. *}
+section {* We now use context in a CBV list machine *}
 
 text {* First, a function that composes a list of contexts. *}
 




